{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:51:44Z","timestamp":1773193904716,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":56,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,4,17]],"date-time":"2021-04-17T00:00:00Z","timestamp":1618617600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-16-1-2913 ,N00014-18-1-2037"],"award-info":[{"award-number":["N00014-16-1-2913 ,N00014-18-1-2037"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"NSF (National Science Foundation)","doi-asserted-by":"publisher","award":["CNS-1703598, OAC-1740210, CNS-1703598, CNS-1763172, CCF-2006948, CNS-2007737, CNS-2006437"],"award-info":[{"award-number":["CNS-1703598, OAC-1740210, CNS-1703598, CNS-1763172, CCF-2006948, CNS-2007737, CNS-2006437"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,4,19]]},"DOI":"10.1145\/3445814.3446735","type":"proceedings-article","created":{"date-parts":[[2021,4,11]],"date-time":"2021-04-11T17:06:26Z","timestamp":1618160786000},"page":"415-428","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":31,"title":["Jaaru: efficiently model checking persistent memory programs"],"prefix":"10.1145","author":[{"given":"Hamed","family":"Gorjiara","sequence":"first","affiliation":[{"name":"University of California at Irvine, USA"}]},{"given":"Guoqing Harry","family":"Xu","sequence":"additional","affiliation":[{"name":"University of California at Los Angeles, USA"}]},{"given":"Brian","family":"Demsky","sequence":"additional","affiliation":[{"name":"University of California at Irvine, USA"}]}],"member":"320","published-online":{"date-parts":[[2021,4,17]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535845"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_28"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276505"},{"key":"e_1_3_2_1_4_1","first-page":"55","volume-title":"Proceedings of the 2016 ACM SIGPLAN International Symposium on Memory Management, ISMM 2016","author":"J.","year":"2016","unstructured":"Hans- J. Boehm and Dhruva R. Chakrabarti. Persistence Programming Models for Non-volatile Memory . In Proceedings of the 2016 ACM SIGPLAN International Symposium on Memory Management, ISMM 2016 , pages 55 - 67 , 2016 . Hans-J. Boehm and Dhruva R. Chakrabarti. Persistence Programming Models for Non-volatile Memory. In Proceedings of the 2016 ACM SIGPLAN International Symposium on Memory Management, ISMM 2016, pages 55-67, 2016."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250737"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS.2018.00046"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660224"},{"key":"e_1_3_2_1_8_1","volume-title":"October","author":"Chatterjee Krishnendu","year":"2019","unstructured":"Krishnendu Chatterjee , Andreas Pavlogiannis , and Viktor Toman . Value-centric dynamic partial order reduction. Proceeding of the ACM on Programming Languages, 3 (OOPSLA) , October 2019 . Krishnendu Chatterjee, Andreas Pavlogiannis, and Viktor Toman. Value-centric dynamic partial order reduction. Proceeding of the ACM on Programming Languages, 3 (OOPSLA), October 2019."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132776"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_3_2_1_11_1","volume-title":"A breakthrough in non-volatile memory technology. https:\/\/www.intel.com\/content\/www\/us\/en\/architecture-andtechnology\/intel-micron-3d-xpoint-webcast.html","author":"Intel Corporation","year":"2018","unstructured":"Intel Corporation . 3 D X Point : A breakthrough in non-volatile memory technology. https:\/\/www.intel.com\/content\/www\/us\/en\/architecture-andtechnology\/intel-micron-3d-xpoint-webcast.html , 2018 . Intel Corporation. 3D XPoint : A breakthrough in non-volatile memory technology. https:\/\/www.intel.com\/content\/www\/us\/en\/architecture-andtechnology\/intel-micron-3d-xpoint-webcast.html, 2018."},{"key":"e_1_3_2_1_12_1","volume-title":"April","author":"Intel Corporation","year":"2019","unstructured":"Intel Corporation . Intel announces broadest product portfolio for moving, storing and processing data. https:\/\/newsroom.intel.com\/news-releases\/intel-datacentric-launch\/#gs.d3t61g , April 2019 . Intel Corporation. Intel announces broadest product portfolio for moving, storing and processing data. https:\/\/newsroom.intel.com\/news-releases\/intel-datacentric-launch\/#gs.d3t61g, April 2019."},{"key":"e_1_3_2_1_13_1","volume-title":"Persistent memory development kit. https:\/\/pmem.io\/pmdk\/","author":"Intel Corporation","year":"2020","unstructured":"Intel Corporation . Persistent memory development kit. https:\/\/pmem.io\/pmdk\/ , 2020 . Intel Corporation. Persistent memory development kit. https:\/\/pmem.io\/pmdk\/, 2020."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814297"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385991"},{"key":"e_1_3_2_1_17_1","first-page":"70","volume-title":"Peter Varman. Continuous Checkpointing of HTM Transactions in NVM. In Proceedings of the 2017 ACM SIGPLAN International Symposium on Memory Management, ISMM '17","author":"Giles Ellis","year":"2017","unstructured":"Ellis Giles , Kshitij Doshi , and Peter Varman. Continuous Checkpointing of HTM Transactions in NVM. In Proceedings of the 2017 ACM SIGPLAN International Symposium on Memory Management, ISMM '17 , pages 70 - 81 , 2017 . Ellis Giles, Kshitij Doshi, and Peter Varman. Continuous Checkpointing of HTM Transactions in NVM. In Proceedings of the 2017 ACM SIGPLAN International Symposium on Memory Management, ISMM '17, pages 70-81, 2017."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/547238"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263717"},{"key":"e_1_3_2_1_20_1","volume-title":"Software model checking: The VeriSoft approach. Formal Methods in System Design, 26 ( 2 ): 77-101","author":"Godefroid Patrice","year":"2005","unstructured":"Patrice Godefroid . Software model checking: The VeriSoft approach. Formal Methods in System Design, 26 ( 2 ): 77-101 , 2005 . Patrice Godefroid. Software model checking: The VeriSoft approach. Formal Methods in System Design, 26 ( 2 ): 77-101, 2005."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192367"},{"key":"e_1_3_2_1_22_1","first-page":"468","volume-title":"Patrick Eugster. NVthreads: Practical Persistence for Multi-threaded Applications. In Proceedings of the 12th European Conference on Computer Systems, EuroSys ' 17","author":"Ching-Hsiang Hsu Terry","year":"2017","unstructured":"Terry Ching-Hsiang Hsu , Helge Br\u00fcgner , Indrajit Roy , Kimberly Keeton , and Patrick Eugster. NVthreads: Practical Persistence for Multi-threaded Applications. In Proceedings of the 12th European Conference on Computer Systems, EuroSys ' 17 , pages 468 - 482 , 2017 . Terry Ching-Hsiang Hsu, Helge Br\u00fcgner, Indrajit Roy, Kimberly Keeton, and Patrick Eugster. NVthreads: Practical Persistence for Multi-threaded Applications. In Proceedings of the 12th European Conference on Computer Systems, EuroSys ' 17, pages 468-482, 2017."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984025"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872410"},{"key":"e_1_3_2_1_25_1","volume-title":"July","author":"Kapela Tomasz","year":"2015","unstructured":"Tomasz Kapela . An introduction to pmemcheck (part 1)-basics. https:\/\/pmem. io\/ 2015 \/07\/17\/pmemcheck-basic.html , July 2015 . Tomasz Kapela. An introduction to pmemcheck (part 1)-basics. https:\/\/pmem. io\/ 2015 \/07\/17\/pmemcheck-basic.html, July 2015."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359662"},{"key":"e_1_3_2_1_27_1","volume-title":"Proceedings of the ACM on Programming Languages, 2 (POPL)","author":"Kokologiannakis Michalis","year":"2017","unstructured":"Michalis Kokologiannakis , Ori Lahav , Konstantinos Sagonas , and Viktor Vafeiadis . Efective stateless model checking for C\/C++ concurrency . Proceedings of the ACM on Programming Languages, 2 (POPL) , December 2017 . Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, and Viktor Vafeiadis. Efective stateless model checking for C\/C++ concurrency. Proceedings of the ACM on Programming Languages, 2 (POPL), December 2017."},{"key":"e_1_3_2_1_28_1","first-page":"256","volume-title":"IEEE International Symposium on Performance Analysis of Systems and Software, ISPASS '13","author":"Kultursay Emre","year":"2013","unstructured":"Emre Kultursay , Mahmut Kandemir , Anand Sivasubramaniam , and Onur Mutlu . Evaluating STT-RAM as an energy-eficient main memory alternative . In IEEE International Symposium on Performance Analysis of Systems and Software, ISPASS '13 , pages 256 - 267 , 2013 . Emre Kultursay, Mahmut Kandemir, Anand Sivasubramaniam, and Onur Mutlu. Evaluating STT-RAM as an energy-eficient main memory alternative. In IEEE International Symposium on Performance Analysis of Systems and Software, ISPASS '13, pages 256-267, 2013."},{"key":"e_1_3_2_1_29_1","first-page":"433","volume-title":"Proceedings of the 2014 USENIX Annual Technical Conference","author":"Lantz Philip","year":"2014","unstructured":"Philip Lantz , Subramanya Dulloor , Sanjay Kumar , Rajesh Sankaran , and Jef Jackson . Yat : A validation framework for persistent memory software . In Proceedings of the 2014 USENIX Annual Technical Conference , pages 433 - 438 , Philadelphia, PA , June 2014 . USENIX Association. Philip Lantz, Subramanya Dulloor, Sanjay Kumar, Rajesh Sankaran, and Jef Jackson. Yat: A validation framework for persistent memory software. In Proceedings of the 2014 USENIX Annual Technical Conference, pages 433-438, Philadelphia, PA, June 2014. USENIX Association."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12029-9_22"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1555754.1555758"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359635"},{"key":"e_1_3_2_1_33_1","first-page":"399","volume-title":"Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation, OSDI ' 14","author":"Leesatapornwongsa Tanakorn","year":"2014","unstructured":"Tanakorn Leesatapornwongsa , Mingzhe Hao , Pallavi Joshi , Jefrey F. Lukman , and Haryadi S. Gunawi . SAMC: Semantic-aware model checking for fast discovery of deep bugs in cloud systems . In Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation, OSDI ' 14 , pages 399 - 414 , USA, 2014 . USENIX Association. Tanakorn Leesatapornwongsa, Mingzhe Hao, Pallavi Joshi, Jefrey F. Lukman, and Haryadi S. Gunawi. SAMC: Semantic-aware model checking for fast discovery of deep bugs in cloud systems. In Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation, OSDI ' 14, pages 399-414, USA, 2014. USENIX Association."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3037697.3037714"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2018.00029"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373376.3378452"},{"key":"e_1_3_2_1_37_1","first-page":"411","volume-title":"Proceedings of the 24th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS '19","author":"Liu Sihang","year":"2019","unstructured":"Sihang Liu , Yizhou Wei , Jishen Zhao , Aasheesh Kolli , and Samira Khan . PMTest : A fast and flexible testing framework for persistent memory programs . In Proceedings of the 24th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS '19 , pages 411 - 425 , New York, NY, USA , 2019 . Association for Computing Machinery. Sihang Liu, Yizhou Wei, Jishen Zhao, Aasheesh Kolli, and Samira Khan. PMTest: A fast and flexible testing framework for persistent memory programs. In Proceedings of the 24th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS '19, pages 411-425, New York, NY, USA, 2019. Association for Computing Machinery."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815422"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/3291168.3291172"},{"key":"e_1_3_2_1_40_1","volume-title":"CHESS: A systematic testing tool for concurrent software. Logic-Based Program Synthesis and Transformation, page","author":"Musuvathi Madan","year":"2007","unstructured":"Madan Musuvathi , Shaz Qadeer , and Thomas Ball . CHESS: A systematic testing tool for concurrent software. Logic-Based Program Synthesis and Transformation, page 16, November 2007 . Madan Musuvathi, Shaz Qadeer, and Thomas Ball. CHESS: A systematic testing tool for concurrent software. Logic-Based Program Synthesis and Transformation, page 16, November 2007."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/1855741.1855760"},{"key":"e_1_3_2_1_42_1","volume-title":"Proceedings of the 14th USENIX Conference on Operating Systems Design and Implementation, OSDI ' 20","author":"Neal Ian","year":"2020","unstructured":"Ian Neal , B. Reeves , Ben Stoler , Andrew Quinn , Youngjin Kwon , S. Peter , and Baris Kasikci . AGAMOTTO : How persistent is your persistent memory application ? In Proceedings of the 14th USENIX Conference on Operating Systems Design and Implementation, OSDI ' 20 , 2020 . Ian Neal, B. Reeves, Ben Stoler, Andrew Quinn, Youngjin Kwon, S. Peter, and Baris Kasikci. AGAMOTTO: How persistent is your persistent memory application ? In Proceedings of the 14th USENIX Conference on Operating Systems Design and Implementation, OSDI ' 20, 2020."},{"key":"e_1_3_2_1_43_1","volume-title":"Proceedings of the ACM on Programming Languages, 4 (POPL)","author":"Raad Azalea","year":"2019","unstructured":"Azalea Raad , John Wickerson , Gil Neiger , and Viktor Vafeiadis . Persistency semantics of the Intel-X86 architecture . Proceedings of the ACM on Programming Languages, 4 (POPL) , December 2019 . Azalea Raad, John Wickerson, Gil Neiger, and Viktor Vafeiadis. Persistency semantics of the Intel-X86 architecture. Proceedings of the ACM on Programming Languages, 4 (POPL), December 2019."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542506"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2012.18"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693017_25"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.5555\/1763218.1763234"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.5555\/3026877.3026879"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30793-5_14"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2012.2190369"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2010.2070050"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2019.00035"},{"key":"e_1_3_2_1_53_1","first-page":"10","volume-title":"Proceedings of the 7th USENIX Symposium on Operating Systems Design and Implementation, OSDI ' 06","author":"Yang Junfeng","year":"2006","unstructured":"Junfeng Yang , Can Sar , and Dawson Engler . Explode : A lightweight, general system for finding serious storage system errors . In Proceedings of the 7th USENIX Symposium on Operating Systems Design and Implementation, OSDI ' 06 , page 10 , USA, 2006 . USENIX Association. Junfeng Yang, Can Sar, and Dawson Engler. Explode: A lightweight, general system for finding serious storage system errors. In Proceedings of the 7th USENIX Symposium on Operating Systems Design and Implementation, OSDI ' 06, page 10, USA, 2006. USENIX Association."},{"key":"e_1_3_2_1_54_1","volume-title":"Using model checking to find serious file system errors. ACM Transactions on Computer Systems, 24 ( 4 )","author":"Yang Junfeng","year":"2006","unstructured":"Junfeng Yang , Paul Twohey , Dawson Engler , and Madanlal Musuvathi . Using model checking to find serious file system errors. ACM Transactions on Computer Systems, 24 ( 4 ) : 393-423, November 2006 . Junfeng Yang, Paul Twohey, Dawson Engler, and Madanlal Musuvathi. Using model checking to find serious file system errors. ACM Transactions on Computer Systems, 24 ( 4 ): 393-423, November 2006."},{"key":"e_1_3_2_1_55_1","volume-title":"Eficient data mapping and bufering techniques for multilevel cell phasechange memories. ACM Transactions on Architecture and Code Optimization, 11 ( 4 ): 40 : 1-40","author":"Yoon Hanbin","year":"2014","unstructured":"Hanbin Yoon , Justin Meza , Naveen Muralimanohar , Norman P. Jouppi , and Onur Mutlu . Eficient data mapping and bufering techniques for multilevel cell phasechange memories. ACM Transactions on Architecture and Code Optimization, 11 ( 4 ): 40 : 1-40 : 25, December 2014 . Hanbin Yoon, Justin Meza, Naveen Muralimanohar, Norman P. Jouppi, and Onur Mutlu. Eficient data mapping and bufering techniques for multilevel cell phasechange memories. ACM Transactions on Architecture and Code Optimization, 11 ( 4 ): 40 : 1-40 : 25, December 2014."},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737956"}],"event":{"name":"ASPLOS '21: 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems","location":"Virtual USA","acronym":"ASPLOS '21","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 26th ACM International Conference on Architectural Support for Programming Languages and Operating Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3445814.3446735","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/abs\/10.1145\/3445814.3446735","content-type":"text\/html","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3445814.3446735","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3445814.3446735","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:28:14Z","timestamp":1750195694000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3445814.3446735"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,4,17]]},"references-count":56,"alternative-id":["10.1145\/3445814.3446735","10.1145\/3445814"],"URL":"https:\/\/doi.org\/10.1145\/3445814.3446735","relation":{},"subject":[],"published":{"date-parts":[[2021,4,17]]},"assertion":[{"value":"2021-04-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}