{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:51:49Z","timestamp":1773193909329,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":42,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,6,8]],"date-time":"2019-06-08T00:00:00Z","timestamp":1559952000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100011199","name":"European Research Council","doi-asserted-by":"publisher","award":["683289"],"award-info":[{"award-number":["683289"]}],"id":[{"id":"10.13039\/100011199","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,6,8]]},"DOI":"10.1145\/3314221.3314609","type":"proceedings-article","created":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T21:02:18Z","timestamp":1559941338000},"page":"96-110","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":70,"title":["Model checking for weakly consistent libraries"],"prefix":"10.1145","author":[{"given":"Michalis","family":"Kokologiannakis","sequence":"first","affiliation":[{"name":"MPI-SWS, Germany"}]},{"given":"Azalea","family":"Raad","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}]},{"given":"Viktor","family":"Vafeiadis","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}]}],"member":"320","published-online":{"date-parts":[[2019,6,8]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535845"},{"key":"e_1_3_2_2_2_1","volume-title":"Stateless Model Checking for TSO and PSO. In TACAS 2015 (LNCS)","volume":"9035","author":"Abdulla Parosh Aziz","year":"2015","unstructured":"Parosh Aziz Abdulla , Stavros Aronis , Mohamed Faouzi Atig , Bengt Jonsson , Carl Leonardsson , and Konstantinos Sagonas . 2015 . Stateless Model Checking for TSO and PSO. In TACAS 2015 (LNCS) , Vol. 9035 . Springer, Berlin, Heidelberg, 353\u2013367. Parosh Aziz Abdulla, Stavros Aronis, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson, and Konstantinos Sagonas. 2015. Stateless Model Checking for TSO and PSO. In TACAS 2015 (LNCS), Vol. 9035. Springer, Berlin, Heidelberg, 353\u2013367."},{"key":"e_1_3_2_2_3_1","volume-title":"Stateless Model Checking for POWER. In CAV 2016 (LNCS)","volume":"9780","author":"Abdulla Parosh Aziz","year":"2016","unstructured":"Parosh Aziz Abdulla , Mohamed Faouzi Atig , Bengt Jonsson , and Carl Leonardsson . 2016 . Stateless Model Checking for POWER. In CAV 2016 (LNCS) , Vol. 9780 . Springer, Berlin, Heidelberg, 134\u2013156. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, and Carl Leonardsson. 2016. Stateless Model Checking for POWER. In CAV 2016 (LNCS), Vol. 9780. Springer, Berlin, Heidelberg, 134\u2013156."},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276505"},{"key":"e_1_3_2_2_5_1","volume-title":"Partial Orders for Efficient Bounded Model Checking of Concurrent Software. In CAV 2013 (LNCS)","volume":"8044","author":"Alglave Jade","year":"2013","unstructured":"Jade Alglave , Daniel Kroening , and Michael Tautschnig . 2013 . Partial Orders for Efficient Bounded Model Checking of Concurrent Software. In CAV 2013 (LNCS) , Vol. 8044 . Springer, Berlin, Heidelberg, 141\u2013157. Jade Alglave, Daniel Kroening, and Michael Tautschnig. 2013. Partial Orders for Efficient Bounded Model Checking of Concurrent Software. In CAV 2013 (LNCS), Vol. 8044. Springer, Berlin, Heidelberg, 141\u2013157."},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_3_2_2_7_1","volume-title":"TACAS (2) (LNCS)","author":"Aronis Stavros","unstructured":"Stavros Aronis , Bengt Jonsson , Magnus L\u00e5ng , and Konstantinos Sagonas . 2018. Optimal Dynamic Partial Order Reduction with Observers . In TACAS (2) (LNCS) , Vol. 10806 . Springer , 229\u2013248. Stavros Aronis, Bengt Jonsson, Magnus L\u00e5ng, and Konstantinos Sagonas. 2018. Optimal Dynamic Partial Order Reduction with Observers. In TACAS (2) (LNCS), Vol. 10806. Springer, 229\u2013248."},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2247684.2247688"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2618128.2618134"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290383"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158119"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1073970.1073974"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814297"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040315"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539794279614"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263717"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-005-1489-x"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737975"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984025"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-014-0150-6"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009850"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158105"},{"key":"e_1_3_2_2_25_1","unstructured":"Michalis Kokologiannakis Azalea Raad and Viktor Vafeiadis. 2019. Technical Appendix. https:\/\/plv.mpi-sws.org\/genmc  Michalis Kokologiannakis Azalea Raad and Viktor Vafeiadis. 2019. Technical Appendix. https:\/\/plv.mpi-sws.org\/genmc"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3092282.3092287"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/7351.7352"},{"key":"e_1_3_2_2_30_1","volume-title":"DATE","author":"Liang L.","year":"2018","unstructured":"L. Liang , P. E. McKenney , D. Kroening , and T. Melham . 2018. Verification of tree-based hierarchical read-copy update in the Linux kernel . In DATE 2018 . 61\u201366. L. Liang, P. E. McKenney, D. Kroening, and T. Melham. 2018. Verification of tree-based hierarchical read-copy update in the Linux kernel. In DATE 2018. 61\u201366."},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040336"},{"key":"e_1_3_2_2_32_1","volume-title":"Petri nets: Applications and relationships to other models of concurrency (LNCS)","author":"Mazurkiewicz Antoni","unstructured":"Antoni Mazurkiewicz . 1987. Trace Theory . In Petri nets: Applications and relationships to other models of concurrency (LNCS) , Vol. 255 . Springer , Berlin, Heidelberg , 279\u2013324. Antoni Mazurkiewicz. 1987. Trace Theory. In Petri nets: Applications and relationships to other models of concurrency (LNCS), Vol. 255. Springer, Berlin, Heidelberg, 279\u2013324."},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/103727.103729"},{"key":"e_1_3_2_2_34_1","volume-title":"Finding and Reproducing Heisenbugs in Concurrent Programs. In OSDI","author":"Musuvathi Madanlal","year":"2008","unstructured":"Madanlal Musuvathi , Shaz Qadeer , Thomas Ball , G\u00e9rard Basler , Piramanayagam Arumuga Nainar , and Iulian Neamtiu . 2008 . Finding and Reproducing Heisenbugs in Concurrent Programs. In OSDI 2008. USENIX Association, 267\u2013280. Madanlal Musuvathi, Shaz Qadeer, Thomas Ball, G\u00e9rard Basler, Piramanayagam Arumuga Nainar, and Iulian Neamtiu. 2008. Finding and Reproducing Heisenbugs in Concurrent Programs. In OSDI 2008. USENIX Association, 267\u2013280."},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509514"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158107"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290381"},{"key":"e_1_3_2_2_39_1","volume-title":"Unfolding-based Partial Order Reduction. In CONCUR 2015 (LIPIcs)","volume":"42","author":"Rodr\u00edguez C\u00e9sar","year":"2015","unstructured":"C\u00e9sar Rodr\u00edguez , Marcelo Sousa , Subodh Sharma , and Daniel Kroening . 2015 . Unfolding-based Partial Order Reduction. In CONCUR 2015 (LIPIcs) , Vol. 42 . Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 456\u2013469. C\u00e9sar Rodr\u00edguez, Marcelo Sousa, Subodh Sharma, and Daniel Kroening. 2015. Unfolding-based Partial Order Reduction. In CONCUR 2015 (LIPIcs), Vol. 42. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 456\u2013469."},{"key":"e_1_3_2_2_40_1","volume-title":"The SPARC architecture manual (version 9)","author":"SPARC International Inc. 1994.","unstructured":"SPARC International Inc. 1994. The SPARC architecture manual (version 9) . Prentice-Hall . SPARC International Inc. 1994. The SPARC architecture manual (version 9). Prentice-Hall."},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509532"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737956"}],"event":{"name":"PLDI '19: 40th ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Phoenix AZ USA","acronym":"PLDI '19","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314609","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3314221.3314609","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:53:22Z","timestamp":1750204402000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314609"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6,8]]},"references-count":42,"alternative-id":["10.1145\/3314221.3314609","10.1145\/3314221"],"URL":"https:\/\/doi.org\/10.1145\/3314221.3314609","relation":{},"subject":[],"published":{"date-parts":[[2019,6,8]]},"assertion":[{"value":"2019-06-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}