{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,8]],"date-time":"2026-10-08T22:21:00Z","timestamp":1791498060262,"version":"4.3.4"},"publisher-location":"New York, NY, USA","reference-count":62,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,10,28]],"date-time":"2023-10-28T00:00:00Z","timestamp":1698451200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"NSF","award":["CCF-213-3160"],"award-info":[{"award-number":["CCF-213-3160"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,10,28]]},"DOI":"10.1145\/3613424.3623785","type":"proceedings-article","created":{"date-parts":[[2023,12,8]],"date-time":"2023-12-08T12:22:15Z","timestamp":1702038135000},"page":"1242-1254","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Rigorous Evaluation of Computer Processors with Statistical Model Checking"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1121-8622","authenticated-orcid":false,"given":"Filip","family":"Mazurek","sequence":"first","affiliation":[{"name":"Duke University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2558-8835","authenticated-orcid":false,"given":"Arya","family":"Tschand","sequence":"additional","affiliation":[{"name":"Duke University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0431-1039","authenticated-orcid":false,"given":"Yu","family":"Wang","sequence":"additional","affiliation":[{"name":"University of Florida, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5357-0117","authenticated-orcid":false,"given":"Miroslav","family":"Pajic","sequence":"additional","affiliation":[{"name":"Duke University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7013-8986","authenticated-orcid":false,"given":"Daniel","family":"Sorin","sequence":"additional","affiliation":[{"name":"Duke University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,12,8]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158668"},{"key":"e_1_3_2_1_2_1","volume-title":"Proc. of Computer Architecture Evaluation Using Commercial Workloads.","author":"Alameldeen R.","year":"2002","unstructured":"A.\u00a0 R. Alameldeen , C.\u00a0 J. Mauer , M. Xu , P.\u00a0 J. Harper , M.\u00a0M.\u00a0 K. Martin , and D.\u00a0 J. Sorin . 2002 . Evaluating Non-deterministic Multi-threaded Commercial Workloads . In Proc. of Computer Architecture Evaluation Using Commercial Workloads. A.\u00a0R. Alameldeen, C.\u00a0J. Mauer, M. Xu, P.\u00a0J. Harper, M.\u00a0M.\u00a0K. Martin, and D.\u00a0J. Sorin. 2002. Evaluating Non-deterministic Multi-threaded Commercial Workloads. In Proc. of Computer Architecture Evaluation Using Commercial Workloads."},{"key":"e_1_3_2_1_3_1","volume-title":"Proceedings of the 9th International Symposium on High-Performance Computer Architecture.","author":"R.","unstructured":"Alaa\u00a0 R. Alameldeen and David\u00a0A. Wood. 2003. Variability in Architectural Simulations of Multi-Threaded Workloads . In Proceedings of the 9th International Symposium on High-Performance Computer Architecture. Alaa\u00a0R. Alameldeen and David\u00a0A. Wood. 2003. Variability in Architectural Simulations of Multi-Threaded Workloads. In Proceedings of the 9th International Symposium on High-Performance Computer Architecture."},{"key":"e_1_3_2_1_4_1","volume-title":"Toward Patient Safety in Closed-Loop Medical Device Systems. In ACM\/IEEE International Conference on Cyber-Physical Systems.","author":"Arney David","year":"2010","unstructured":"David Arney , Miroslav Pajic , Julian\u00a0 M. Goldman , Insup Lee , Rahul Mangharam , and Oleg Sokolsky . 2010 . Toward Patient Safety in Closed-Loop Medical Device Systems. In ACM\/IEEE International Conference on Cyber-Physical Systems. David Arney, Miroslav Pajic, Julian\u00a0M. Goldman, Insup Lee, Rahul Mangharam, and Oleg Sokolsky. 2010. Toward Patient Safety in Closed-Loop Medical Device Systems. In ACM\/IEEE International Conference on Cyber-Physical Systems."},{"key":"e_1_3_2_1_5_1","volume-title":"Proc. of the 5th Annual Workshop on Modeling, Benchmarking and Simulation.","author":"Bienia C.","unstructured":"C. Bienia and K. Li . 2009. PARSEC 2.0: A New Benchmark Suite for Chip-Multiprocessors . In Proc. of the 5th Annual Workshop on Modeling, Benchmarking and Simulation. C. Bienia and K. Li. 2009. PARSEC 2.0: A New Benchmark Suite for Chip-Multiprocessors. In Proc. of the 5th Annual Workshop on Modeling, Benchmarking and Simulation."},{"key":"e_1_3_2_1_6_1","volume-title":"Enabling Reproducible and Agile Full-System Simulation. In IEEE Int\u2019l Symp. on Performance Analysis of Systems and Software.","author":"Bruce R.","unstructured":"B.\u00a0 R. Bruce , A. Akram , H. Nguyen , K. Roarty , M. Samani , M. Friborz , T. Reddy , M.\u00a0 D. Sinclair , and J. Lowe-Power . 2021 . Enabling Reproducible and Agile Full-System Simulation. In IEEE Int\u2019l Symp. on Performance Analysis of Systems and Software. B.\u00a0R. Bruce, A. Akram, H. Nguyen, K. Roarty, M. Samani, M. Friborz, T. Reddy, M.\u00a0D. Sinclair, and J. Lowe-Power. 2021. Enabling Reproducible and Agile Full-System Simulation. In IEEE Int\u2019l Symp. on Performance Analysis of Systems and Software."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1890\/1540-9295(2003)001[0412:AGITQR]2.0.CO;2"},{"key":"e_1_3_2_1_8_1","volume-title":"Sniper: Exploring the Level of Abstraction for Scalable and Accurate Parallel Multi-Core Simulation. In SC.","author":"Carlson E.","year":"2011","unstructured":"T.\u00a0 E. Carlson , W. Heirman , and L. Eeckhout . 2011 . Sniper: Exploring the Level of Abstraction for Scalable and Accurate Parallel Multi-Core Simulation. In SC. T.\u00a0E. Carlson, W. Heirman, and L. Eeckhout. 2011. Sniper: Exploring the Level of Abstraction for Scalable and Accurate Parallel Multi-Core Simulation. In SC."},{"key":"e_1_3_2_1_9_1","unstructured":"G. Casella and R.\u00a0L Berger. 2021. Statistical inference. Cengage Learning.  G. Casella and R.\u00a0L Berger. 2021. Statistical inference. Cengage Learning."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/HPCA.2012.6169043"},{"key":"e_1_3_2_1_11_1","volume-title":"NUSMV: A New Symbolic Model Checker. International Journal of Software Tools for Technology Transfer","author":"Cimatti A.","year":"2000","unstructured":"A. Cimatti , E. Clarke , F. Giunchiglia , and M. Roveri . 2000 . NUSMV: A New Symbolic Model Checker. International Journal of Software Tools for Technology Transfer (2000). A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri. 2000. NUSMV: A New Symbolic Model Checker. International Journal of Software Tools for Technology Transfer (2000)."},{"key":"e_1_3_2_1_12_1","volume-title":"Temporal Logics for Hyperproperties. In International Conference on Principles of Security and Trust.","author":"Clarkson R.","unstructured":"M.\u00a0 R. Clarkson , B. Finkbeiner , M. Koleini , K.\u00a0 K. Micinski , M.\u00a0 N. Rabe , and C. Sanchez . 2014 . Temporal Logics for Hyperproperties. In International Conference on Principles of Security and Trust. M.\u00a0R. Clarkson, B. Finkbeiner, M. Koleini, K.\u00a0K. Micinski, M.\u00a0N. Rabe, and C. Sanchez. 2014. Temporal Logics for Hyperproperties. In International Conference on Principles of Security and Trust."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1093\/biomet\/26.4.404"},{"key":"e_1_3_2_1_14_1","volume-title":"Estimating and Understanding Architectural Risk. In International Symposium on Microarchitecture.","author":"Cui Weilong","year":"2017","unstructured":"Weilong Cui and Timothy Sherwood . 2017 . Estimating and Understanding Architectural Risk. In International Symposium on Microarchitecture. Weilong Cui and Timothy Sherwood. 2017. Estimating and Understanding Architectural Risk. In International Symposium on Microarchitecture."},{"key":"e_1_3_2_1_15_1","volume-title":"Proc. 19th International Conference on DNA Computing and Molecular Programming.","author":"Dannenberg F.","unstructured":"F. Dannenberg , M. Kwiatkowska , C. Thachuk , and A. Turberfield . 2013. DNA Walker Circuits: Computational Potential, Design, and Verification . In Proc. 19th International Conference on DNA Computing and Molecular Programming. F. Dannenberg, M. Kwiatkowska, C. Thachuk, and A. Turberfield. 2013. DNA Walker Circuits: Computational Potential, Design, and Verification. In Proc. 19th International Conference on DNA Computing and Molecular Programming."},{"key":"e_1_3_2_1_16_1","volume-title":"Uppaal SMC Tutorial. Int\u2019l Journal of Software Tools for Technology Transfer","author":"David A.","year":"2015","unstructured":"A. David , K.\u00a0 G. Larsen , A. Legay , M. Miku\u0103ionis , and D.\u00a0 B. Poulsen . 2015. Uppaal SMC Tutorial. Int\u2019l Journal of Software Tools for Technology Transfer ( 2015 ). A. David, K.\u00a0G. Larsen, A. Legay, M. Miku\u0103ionis, and D.\u00a0B. Poulsen. 2015. Uppaal SMC Tutorial. Int\u2019l Journal of Software Tools for Technology Transfer (2015)."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"crossref","unstructured":"C. Daws M. Kwiatkowska and G. Norman. 2004. Automatic Verification of the IEEE 1394 Root Contention Protocol with KRONOS and PRISM. International Journal of Network Security and Its Applications 5 (2004).  C. Daws M. Kwiatkowska and G. Norman. 2004. Automatic Verification of the IEEE 1394 Root Contention Protocol with KRONOS and PRISM. International Journal of Network Security and Its Applications 5 (2004).","DOI":"10.1007\/s10009-003-0118-5"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Augusto\u00a0Born De\u00a0Oliveira Sebastian Fischmeister Amer Diwan Matthias Hauswirth and Peter\u00a0F Sweeney. 2013. Why you should care about quantile regression. In Architectural Support for Programming Languages and Operating Systems ASPLOS \u201913. 207\u2013218. http:\/\/dl.acm.org\/citation.cfm?doid=2451116.2451140  Augusto\u00a0Born De\u00a0Oliveira Sebastian Fischmeister Amer Diwan Matthias Hauswirth and Peter\u00a0F Sweeney. 2013. Why you should care about quantile regression. In Architectural Support for Programming Languages and Operating Systems ASPLOS \u201913. 207\u2013218. http:\/\/dl.acm.org\/citation.cfm?doid=2451116.2451140","DOI":"10.1145\/2499368.2451140"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"crossref","unstructured":"David\u00a0L Dill. 1996. The Murphi Verification System. In CAV Vol.\u00a01102.  David\u00a0L Dill. 1996. The Murphi Verification System. In CAV Vol.\u00a01102.","DOI":"10.1007\/3-540-61474-5_86"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"crossref","unstructured":"M. Duflot M. Kwiatkowska G. Norman and D. Parker. 2006. A Formal Analysis of Bluetooth Device Discovery. International Journal of Software Tools for Technology Transfer (2006).  M. Duflot M. Kwiatkowska G. Norman and D. Parker. 2006. A Formal Analysis of Bluetooth Device Discovery. International Journal of Software Tools for Technology Transfer (2006).","DOI":"10.1007\/s10009-006-0014-x"},{"key":"e_1_3_2_1_21_1","first-page":"288","article-title":"An introduction to the bootstrap. Chapman and Hall, New York, NY. Farrell, J., Johnston, M. and Twynam, D.(1998),\u2018\u2018Volunteer motivation, satisfaction, and management at an elite sporting competition\u2019","volume":"12","author":"Efron B.","year":"1993","unstructured":"B. Efron and Tibshirani R.J. 1993 . An introduction to the bootstrap. Chapman and Hall, New York, NY. Farrell, J., Johnston, M. and Twynam, D.(1998),\u2018\u2018Volunteer motivation, satisfaction, and management at an elite sporting competition\u2019 \u2019, Journal of Sport Management 12 (1993), 288 \u2013 300 . B. Efron and Tibshirani R.J.1993. An introduction to the bootstrap. Chapman and Hall, New York, NY. Farrell, J., Johnston, M. and Twynam, D.(1998),\u2018\u2018Volunteer motivation, satisfaction, and management at an elite sporting competition\u2019\u2019, Journal of Sport Management 12 (1993), 288\u2013300.","journal-title":"Journal of Sport Management"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"crossref","unstructured":"M. Elboukhari A. Azizi and M. Azizi. 2010. Analysis of the Security of BB84 by Model Checking. Int\u2019l Journal of Network Security and Its Applications 2 (2010).  M. Elboukhari A. Azizi and M. Azizi. 2010. Analysis of the Security of BB84 by Model Checking. Int\u2019l Journal of Network Security and Its Applications 2 (2010).","DOI":"10.5121\/ijnsa.2010.2207"},{"key":"e_1_3_2_1_23_1","volume-title":"Proceedings of the ACM\/IEEE Sixth International Conference on Cyber-Physical Systems.","author":"Feng L.","unstructured":"L. Feng , C. Wiltsche , L. Humphrey , and U. Topcu . 2015. Controller Synthesis for Autonomous Systems Interacting with Human Operators . In Proceedings of the ACM\/IEEE Sixth International Conference on Cyber-Physical Systems. L. Feng, C. Wiltsche, L. Humphrey, and U. Topcu. 2015. Controller Synthesis for Autonomous Systems Interacting with Human Operators. In Proceedings of the ACM\/IEEE Sixth International Conference on Cyber-Physical Systems."},{"key":"e_1_3_2_1_24_1","volume-title":"Formal Methods for the Analysis of Wireless Network Protocols. Ph.\u00a0D. Dissertation","author":"Fruth M.","unstructured":"M. Fruth . 2011. Formal Methods for the Analysis of Wireless Network Protocols. Ph.\u00a0D. Dissertation . University of Oxford. M. Fruth. 2011. Formal Methods for the Analysis of Wireless Network Protocols. Ph.\u00a0D. Dissertation. University of Oxford."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297105.1297033"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04898-2_420"},{"key":"e_1_3_2_1_27_1","first-page":"81","article-title":"What is not what in statistics. Journal of the Royal Statistical Society","volume":"26","author":"Guttman Louis","year":"1977","unstructured":"Louis Guttman . 1977 . What is not what in statistics. Journal of the Royal Statistical Society . Series D (The Statistician) 26 , 2 (1977), 81 \u2013 107 . Louis Guttman. 1977. What is not what in statistics. Journal of the Royal Statistical Society. Series D (The Statistician) 26, 2 (1977), 81\u2013107.","journal-title":"Series D (The Statistician)"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"crossref","unstructured":"H. Hansson and B. Jonsson. 1994. A Logic for Reasoning About Time and Reliability. Formal Aspects of Computing 6 5 (1994).  H. Hansson and B. Jonsson. 1994. A Logic for Reasoning About Time and Reliability. Formal Aspects of Computing 6 5 (1994).","DOI":"10.1007\/BF01211866"},{"key":"e_1_3_2_1_29_1","volume-title":"Proc. of the Second Asia-Pacific Workshop on Systems. 1\u20135.","author":"Harji S.","unstructured":"A.\u00a0 S. Harji , P.\u00a0 A. Buhr , and T. Brecht . 2011. Our troubles with Linux and why you should care . In Proc. of the Second Asia-Pacific Workshop on Systems. 1\u20135. A.\u00a0S. Harji, P.\u00a0A. Buhr, and T. Brecht. 2011. Our troubles with Linux and why you should care. In Proc. of the Second Asia-Pacific Workshop on Systems. 1\u20135."},{"key":"e_1_3_2_1_30_1","volume-title":"Computer Comparisons in the Presence of Performance Variation. Frontiers of Computer Science 14, 1","author":"Irving Samuel","year":"2020","unstructured":"Samuel Irving , Bin Li , Shaoming Chen , Lu Peng , Weihua Zhang , and Lide Duan . 2020. Computer Comparisons in the Presence of Performance Variation. Frontiers of Computer Science 14, 1 ( 2020 ). Samuel Irving, Bin Li, Shaoming Chen, Lu Peng, Weihua Zhang, and Lide Duan. 2020. Computer Comparisons in the Presence of Performance Variation. Frontiers of Computer Science 14, 1 (2020)."},{"key":"e_1_3_2_1_31_1","volume-title":"Proc. of the 2005 Int\u2019l Symposium on Performance Evaluation of Computer and Telecommunication Systems.","author":"Kalibera Tomas","year":"2005","unstructured":"Tomas Kalibera , Lubomir Bulej , and Petr Tuma . 2005 . Benchmark precision and random initial state . In Proc. of the 2005 Int\u2019l Symposium on Performance Evaluation of Computer and Telecommunication Systems. Tomas Kalibera, Lubomir Bulej, and Petr Tuma. 2005. Benchmark precision and random initial state. In Proc. of the 2005 Int\u2019l Symposium on Performance Evaluation of Computer and Telecommunication Systems."},{"key":"e_1_3_2_1_32_1","unstructured":"Tomas Kalibera and Richard Jones. 2020. Quantifying Performance Changes with Effect Size Confidence Intervals. arxiv:2007.10899\u00a0[stat.ME]  Tomas Kalibera and Richard Jones. 2020. Quantifying Performance Changes with Effect Size Confidence Intervals. arxiv:2007.10899\u00a0[stat.ME]"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1257\/jep.15.4.143"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"crossref","unstructured":"M. Kwiatkowska and G. Norman. 2002. Verifying Randomized Byzantine Agreement. In Formal Techniques for Networked and Distributed Systems.  M. Kwiatkowska and G. Norman. 2002. Verifying Randomized Byzantine Agreement. In Formal Techniques for Networked and Distributed Systems.","DOI":"10.1007\/3-540-36135-9_13"},{"key":"e_1_3_2_1_35_1","volume-title":"Probabilistic Model Checking and Power-Aware Computing. In 7th International Workshop on Performability Modeling of Computer and Communication Systems.","author":"Kwiatkowska M.","unstructured":"M. Kwiatkowska , G. Norman , and D. Parker . 2005 . Probabilistic Model Checking and Power-Aware Computing. In 7th International Workshop on Performability Modeling of Computer and Communication Systems. M. Kwiatkowska, G. Norman, and D. Parker. 2005. Probabilistic Model Checking and Power-Aware Computing. In 7th International Workshop on Performability Modeling of Computer and Communication Systems."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"crossref","unstructured":"M. Kwiatkowska G. Norman and D. Parker. 2006. Controller Dependability Analysis by Probabilistic Model Checking. Control Engineering Practice 15 (2006).  M. Kwiatkowska G. Norman and D. Parker. 2006. Controller Dependability Analysis by Probabilistic Model Checking. Control Engineering Practice 15 (2006).","DOI":"10.1016\/j.conengprac.2006.07.003"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"crossref","unstructured":"M. Kwiatkowska G. Norman and D. Parker. 2008. Using Probabilistic Model Checking in Systems Biology. ACM SIGMETRICS Performance Evaluation Review 35 (2008).  M. Kwiatkowska G. Norman and D. Parker. 2008. Using Probabilistic Model Checking in Systems Biology. ACM SIGMETRICS Performance Evaluation Review 35 (2008).","DOI":"10.1145\/1364644.1364651"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"crossref","unstructured":"M. Kwiatkowska G. Norman and D. Parker. 2011. Computer Aided Verification. Springer Berlin Heidelberg Chapter PRISM 4.0: Verification of Probabilistic Real-time Systems.  M. Kwiatkowska G. Norman and D. Parker. 2011. Computer Aided Verification. Springer Berlin Heidelberg Chapter PRISM 4.0: Verification of Probabilistic Real-time Systems.","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"crossref","unstructured":"M. Kwiatkowska G. Norman and D. Parker. 2012. Probabilistic Verification of Herman\u2019s Self-Stabilisation Algorithm. Formal Aspects of Computing 24 (2012).  M. Kwiatkowska G. Norman and D. Parker. 2012. Probabilistic Verification of Herman\u2019s Self-Stabilisation Algorithm. Formal Aspects of Computing 24 (2012).","DOI":"10.1007\/s00165-012-0227-6"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"crossref","unstructured":"Marta Kwiatkowska Gethin Norman and David Parker. 2018. Probabilistic Model Checking: Advances and Applications. In Formal System Verification: State-of the-Art and Future Trends. 73\u2013121.  Marta Kwiatkowska Gethin Norman and David Parker. 2018. Probabilistic Model Checking: Advances and Applications. In Formal System Verification: State-of the-Art and Future Trends. 73\u2013121.","DOI":"10.1007\/978-3-319-57685-5_3"},{"key":"e_1_3_2_1_41_1","unstructured":"A. Legay B. Delahaye and S. Bensalem. 2010. Statistical model checking: An overview. In Runtime Verification Howard Barringer Ylies Falcone Bernd Finkbeiner Klaus Havelund Insup Lee Gordon Pace Grigore Ro\u015fu Oleg Sokolsky and Nikolai Tillmann (Eds.). Vol.\u00a06418. Springer Berlin Heidelberg.  A. Legay B. Delahaye and S. Bensalem. 2010. Statistical model checking: An overview. In Runtime Verification Howard Barringer Ylies Falcone Bernd Finkbeiner Klaus Havelund Insup Lee Gordon Pace Grigore Ro\u015fu Oleg Sokolsky and Nikolai Tillmann (Eds.). Vol.\u00a06418. Springer Berlin Heidelberg."},{"key":"e_1_3_2_1_42_1","unstructured":"J. Lowe-Power A.\u00a0M. Ahmad A. Akram M. Alian R. Amslinger M. Andreozzi A. Armejach N. Asmussen B. Beckmann S. Bharadwaj G. Black G. Bloom B.\u00a0R. Bruce D.\u00a0Rodrigues Carvalho J. Castrillon L. Chen N. Derumigny S. Diestelhorst W. Elsasser C. Escuin M. Fariborz A. Farmahini-Farahani P. Fotouhi R. Gambord J. Gandhi D. Gope T. Grass A. Gutierrez B. Hanindhito A. Hansson S. Haria A. Harris T. Hayes A. Herrera M. Horsnell S.\u00a0Ali\u00a0Raza Jafri R. Jagtap H. Jang R. Jeyapaul T.\u00a0M. Jones M. Jung S. Kannoth H. Khaleghzadeh Y. Kodama T. Krishna T. Marinelli C. Menard A. Mondelli M. Moreto T. M\u00fcck O. Naji K. Nathella H. Nguyen N. Nikoleris L.\u00a0E. Olson M. Orr B. Pham P. Prieto T. Reddy A. Roelke M. Samani A. Sandberg J. Setoain B. Shingarov M.\u00a0D. Sinclair T. Ta R. Thakur G. Travaglini M. Upton N. Vaish I. Vougioukas W. Wang Z. Wang N. Wehn C. Weis D.\u00a0A. Wood H. Yoon and \u00c9.\u00a0F. Zulian. 2020. The gem5 Simulator: Version 20.0+. arxiv:2007.03152\u00a0[cs.AR]  J. Lowe-Power A.\u00a0M. Ahmad A. Akram M. Alian R. Amslinger M. Andreozzi A. Armejach N. Asmussen B. Beckmann S. Bharadwaj G. Black G. Bloom B.\u00a0R. Bruce D.\u00a0Rodrigues Carvalho J. Castrillon L. Chen N. Derumigny S. Diestelhorst W. Elsasser C. Escuin M. Fariborz A. Farmahini-Farahani P. Fotouhi R. Gambord J. Gandhi D. Gope T. Grass A. Gutierrez B. Hanindhito A. Hansson S. Haria A. Harris T. Hayes A. Herrera M. Horsnell S.\u00a0Ali\u00a0Raza Jafri R. Jagtap H. Jang R. Jeyapaul T.\u00a0M. Jones M. Jung S. Kannoth H. Khaleghzadeh Y. Kodama T. Krishna T. Marinelli C. Menard A. Mondelli M. Moreto T. M\u00fcck O. Naji K. Nathella H. Nguyen N. Nikoleris L.\u00a0E. Olson M. Orr B. Pham P. Prieto T. Reddy A. Roelke M. Samani A. Sandberg J. Setoain B. Shingarov M.\u00a0D. Sinclair T. Ta R. Thakur G. Travaglini M. Upton N. Vaish I. Vougioukas W. Wang Z. Wang N. Wehn C. Weis D.\u00a0A. Wood H. Yoon and \u00c9.\u00a0F. Zulian. 2020. The gem5 Simulator: Version 20.0+. arxiv:2007.03152\u00a0[cs.AR]"},{"key":"e_1_3_2_1_43_1","volume-title":"Seventh ACM-IEEE Int\u2019l Conference on Formal Methods and Models for Codesign.","author":"Lungu A.","unstructured":"A. Lungu , P. Bose , D. Sorin , S. German , and G. Janssen . 2009. Multicore Power Management: Ensuring Robustness via Early-Stage Formal Verification . In Seventh ACM-IEEE Int\u2019l Conference on Formal Methods and Models for Codesign. A. Lungu, P. Bose, D. Sorin, S. German, and G. Janssen. 2009. Multicore Power Management: Ensuring Robustness via Early-Stage Formal Verification. In Seventh ACM-IEEE Int\u2019l Conference on Formal Methods and Models for Codesign."},{"key":"e_1_3_2_1_45_1","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"Maler Oded","unstructured":"Oded Maler and Dejan Nickovic . 2004. Monitoring temporal properties of continuous signals . In Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems . Springer , 152\u2013166. Oded Maler and Dejan Nickovic. 2004. Monitoring temporal properties of continuous signals. In Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems. Springer, 152\u2013166."},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"crossref","unstructured":"G. Norman D. Parker M. Kwiatkowska and S. Shukla. 2005. Evaluating the Reliability of NAND Multiplexing with PRISM. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 24 (2005).  G. Norman D. Parker M. Kwiatkowska and S. Shukla. 2005. Evaluating the Reliability of NAND Multiplexing with PRISM. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 24 (2005).","DOI":"10.1109\/TCAD.2005.852033"},{"key":"e_1_3_2_1_47_1","volume-title":"Using Probabilistic Model Checking for Dynamic Power Management. In 3rd Workshop on Automated Verification of Critical Systems.","author":"Norman G.","unstructured":"G. Norman , D. Parker , M. Kwiatkowska , S. Shukla , and R. Gupta . 2003 . Using Probabilistic Model Checking for Dynamic Power Management. In 3rd Workshop on Automated Verification of Critical Systems. G. Norman, D. Parker, M. Kwiatkowska, S. Shukla, and R. Gupta. 2003. Using Probabilistic Model Checking for Dynamic Power Management. In 3rd Workshop on Automated Verification of Critical Systems."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"crossref","unstructured":"G. Norman and V. Shmatikov. 2006. Analysis of Probabilistic Contract Signing. Journal of Computer Security 14 (2006).  G. Norman and V. Shmatikov. 2006. Analysis of Probabilistic Contract Signing. Journal of Computer Security 14 (2006).","DOI":"10.3233\/JCS-2006-14604"},{"key":"e_1_3_2_1_49_1","volume-title":"HeteroGen: Automatic Synthesis of Heterogeneous Cache Coherence Protocols. In IEEE Int\u2019l Symposium on High-Performance Computer Architecture.","author":"Oswald N.","unstructured":"N. Oswald , V. Nagarajan , D.\u00a0 J. Sorin , V. Gavrielatos , T. Olausson , and R. Carr . 2022 . HeteroGen: Automatic Synthesis of Heterogeneous Cache Coherence Protocols. In IEEE Int\u2019l Symposium on High-Performance Computer Architecture. N. Oswald, V. Nagarajan, D.\u00a0J. Sorin, V. Gavrielatos, T. Olausson, and R. Carr. 2022. HeteroGen: Automatic Synthesis of Heterogeneous Cache Coherence Protocols. In IEEE Int\u2019l Symposium on High-Performance Computer Architecture."},{"key":"e_1_3_2_1_50_1","volume-title":"The Temporal Logic of Programs. In 18th Annual Symposium on Foundations of Computer Science.","author":"Pnueli A.","year":"1977","unstructured":"A. Pnueli . 1977 . The Temporal Logic of Programs. In 18th Annual Symposium on Foundations of Computer Science. A. Pnueli. 1977. The Temporal Logic of Programs. In 18th Annual Symposium on Foundations of Computer Science."},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2086696.2086725"},{"key":"e_1_3_2_1_52_1","volume-title":"Computational Sprinting. In Proc. of the 18th Symp. on High Performance Computer Architecture.","author":"Raghavan A.","year":"2012","unstructured":"A. Raghavan , Y. Luo , A. Chandawalla , M. Papaefthymiou , K.\u00a0 P. Pipe , T.\u00a0 F. Wenisch , and M.\u00a0M.\u00a0 K. Martin . 2012 . Computational Sprinting. In Proc. of the 18th Symp. on High Performance Computer Architecture. A. Raghavan, Y. Luo, A. Chandawalla, M. Papaefthymiou, K.\u00a0P. Pipe, T.\u00a0F. Wenisch, and M.\u00a0M.\u00a0K. Martin. 2012. Computational Sprinting. In Proc. of the 18th Symp. on High Performance Computer Architecture."},{"key":"e_1_3_2_1_53_1","volume-title":"Statistical Verification of the Toyota Powertrain Control Verification Benchmark. In ACM Int\u2019l Conference on Hybrid Systems: Computation and Control.","author":"Roohi N.","unstructured":"N. Roohi , Y. Wang , M. West , G.\u00a0 E. Dullerud , and M. Viswanathan . 2017 . Statistical Verification of the Toyota Powertrain Control Verification Benchmark. In ACM Int\u2019l Conference on Hybrid Systems: Computation and Control. N. Roohi, Y. Wang, M. West, G.\u00a0E. Dullerud, and M. Viswanathan. 2017. Statistical Verification of the Toyota Powertrain Control Verification Benchmark. In ACM Int\u2019l Conference on Hybrid Systems: Computation and Control."},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976740"},{"key":"e_1_3_2_1_55_1","volume-title":"Proceedings of the 52nd Annual IEEE\/ACM International Symposium on Computer Architecture.","author":"Shahrad M.","unstructured":"M. Shahrad , J. Balkind , and D. Wentzlaff . 2019. Architectural Implications of Function-as-a-Service Computing . In Proceedings of the 52nd Annual IEEE\/ACM International Symposium on Computer Architecture. M. Shahrad, J. Balkind, and D. Wentzlaff. 2019. Architectural Implications of Function-as-a-Service Computing. In Proceedings of the 52nd Annual IEEE\/ACM International Symposium on Computer Architecture."},{"key":"e_1_3_2_1_56_1","volume-title":"Proc. of the Tenth Int\u2019l Conference on Architectural Support for Programming Languages and Operating Systems.","author":"Sherwood T.","unstructured":"T. Sherwood , E. Perelman , G. Hamerly , and B. Calder . 2002. Automatically Characterizing Large Scale Program Behavior . In Proc. of the Tenth Int\u2019l Conference on Architectural Support for Programming Languages and Operating Systems. T. Sherwood, E. Perelman, G. Hamerly, and B. Calder. 2002. Automatically Characterizing Large Scale Program Behavior. In Proc. of the Tenth Int\u2019l Conference on Architectural Support for Programming Languages and Operating Systems."},{"key":"e_1_3_2_1_57_1","volume-title":"Proceedings of the Twelfth International Conference on VLSI Design.","author":"Srinivasan S.","unstructured":"S. Srinivasan , P.S. Chhabra , P.K. Jaini , A. Aziz , and L. John . 1999. Formal verification of a snoop-based cache coherence protocol using symbolic model checking . In Proceedings of the Twelfth International Conference on VLSI Design. S. Srinivasan, P.S. Chhabra, P.K. Jaini, A. Aziz, and L. John. 1999. Formal verification of a snoop-based cache coherence protocol using symbolic model checking. In Proceedings of the Twelfth International Conference on VLSI Design."},{"key":"e_1_3_2_1_58_1","volume-title":"Isolation-Safe Speculative Access Control for Hardware Transactional Memory. In 25th IEEE Int\u2019l Conference on Electronics, Circuits and Systems.","author":"Tajimi T.","unstructured":"T. Tajimi , M. Hayashi , Y. Futamase , R. Shioya , M. Goshima , and T. Tsumura . 2018 . Isolation-Safe Speculative Access Control for Hardware Transactional Memory. In 25th IEEE Int\u2019l Conference on Electronics, Circuits and Systems. T. Tajimi, M. Hayashi, Y. Futamase, R. Shioya, M. Goshima, and T. Tsumura. 2018. Isolation-Safe Speculative Access Control for Hardware Transactional Memory. In 25th IEEE Int\u2019l Conference on Electronics, Circuits and Systems."},{"key":"e_1_3_2_1_59_1","volume-title":"Proc. of the Ninth ACM Int\u2019l Conf. on Embedded Software.","author":"Vitek J.","unstructured":"J. Vitek and T. Kalibera . 2011. Repeatability, Reproducibility, and Rigor in Systems Research . In Proc. of the Ninth ACM Int\u2019l Conf. on Embedded Software. J. Vitek and T. Kalibera. 2011. Repeatability, Reproducibility, and Rigor in Systems Research. In Proc. of the Ninth ACM Int\u2019l Conf. on Embedded Software."},{"key":"e_1_3_2_1_60_1","doi-asserted-by":"crossref","unstructured":"Y. Wang M. Zarei B. Bonakdarpour and M. Pajic. 2019. Statistical Verification of Hyperproperties for Cyber-Physical Systems. ACM Transactions on Embedded Computing Systems 18 (2019).  Y. Wang M. Zarei B. Bonakdarpour and M. Pajic. 2019. Statistical Verification of Hyperproperties for Cyber-Physical Systems. ACM Transactions on Embedded Computing Systems 18 (2019).","DOI":"10.1145\/3358232"},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/859618.859629"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"crossref","unstructured":"H. Younes G.\u00a0Norman M.\u00a0Kwiatkowska and D. Parker. 2006. Numerical vs. Statistical Probabilistic Model Checking. International Journal on Software Tools for Technology Transfer 8 (2006).  H. Younes G.\u00a0Norman M.\u00a0Kwiatkowska and D. Parker. 2006. Numerical vs. Statistical Probabilistic Model Checking. International Journal on Software Tools for Technology Transfer 8 (2006).","DOI":"10.1007\/s10009-005-0187-8"},{"key":"e_1_3_2_1_63_1","volume-title":"Statistical Verification of Learning-Based Cyber-Physical Systems. In ACM International Conference on Hybrid Systems: Computation and Control.","author":"Zarei M.","unstructured":"M. Zarei , Y. Wang , and M. Pajic . 2020 . Statistical Verification of Learning-Based Cyber-Physical Systems. In ACM International Conference on Hybrid Systems: Computation and Control. M. Zarei, Y. Wang, and M. Pajic. 2020. Statistical Verification of Learning-Based Cyber-Physical Systems. In ACM International Conference on Hybrid Systems: Computation and Control."}],"event":{"name":"MICRO '23: 56th Annual IEEE\/ACM International Symposium on Microarchitecture","location":"Toronto ON Canada","acronym":"MICRO '23","sponsor":["SIGMICRO ACM Special Interest Group on Microarchitectural Research and Processing"]},"container-title":["56th Annual IEEE\/ACM International Symposium on Microarchitecture"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3613424.3623785","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3613424.3623785","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T12:36:30Z","timestamp":1750163790000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3613424.3623785"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,28]]},"references-count":62,"alternative-id":["10.1145\/3613424.3623785","10.1145\/3613424"],"URL":"https:\/\/doi.org\/10.1145\/3613424.3623785","relation":{},"subject":[],"published":{"date-parts":[[2023,10,28]]},"assertion":[{"value":"2023-12-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}