{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T18:19:06Z","timestamp":1784830746774,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":51,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,1]]},"DOI":"10.1145\/3009837.3009893","type":"proceedings-article","created":{"date-parts":[[2016,12,22]],"date-time":"2016-12-22T16:20:29Z","timestamp":1482423629000},"page":"473-485","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":21,"title":["Thread modularity at many levels: a pearl in compositional verification"],"prefix":"10.1145","author":[{"given":"Jochen","family":"Hoenicke","sequence":"first","affiliation":[{"name":"University of Freiburg, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rupak","family":"Majumdar","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andreas","family":"Podelski","sequence":"additional","affiliation":[{"name":"University of Freiburg, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2017,1]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/203095.201069"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2843"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_7"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_28"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0406-x"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/1642724"},{"key":"e_1_3_2_1_7_1","volume-title":"CAV","author":"Arons Tamarah","year":"2001","unstructured":"Tamarah Arons , Amir Pnueli , Sitvanit Ruah , Jiazhao Xu , and Lenore D. Zuck . Parameterized verification with automatically computed inductive assertions . In CAV , 2001 . Tamarah Arons, Amir Pnueli, Sitvanit Ruah, Jiazhao Xu, and Lenore D. Zuck. Parameterized verification with automatically computed inductive assertions. In CAV, 2001."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(75)80018-3"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-002-0095-0"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_37"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_37"},{"key":"e_1_3_2_1_12_1","volume-title":"Personal communication","author":"Black David L.","year":"2016","unstructured":"David L. Black . Personal communication ., 2016 . David L. Black. Personal communication., 2016."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/70082.68193"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-008-0063-8"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_16_1","volume-title":"Institut National Polytechnique de Lorraine","author":"Cousot Patrick","year":"1980","unstructured":"Patrick Cousot and Radhia Cousot . Reasoning about program invariance proof methods. Res. rep. CRIN-80-P050, Centre de Recherche en Informatique de Nancy (CRIN) , Institut National Polytechnique de Lorraine , Nancy, France , July 1980 . Patrick Cousot and Radhia Cousot. Reasoning about program invariance proof methods. Res. rep. CRIN-80-P050, Centre de Recherche en Informatique de Nancy (CRIN), Institut National Polytechnique de Lorraine, Nancy, France, July 1980."},{"key":"e_1_3_2_1_17_1","volume-title":"Automatic program construction techniques","author":"Cousot Patrick","year":"1984","unstructured":"Patrick Cousot and Radhia Cousot . Invariance proof methods and analysis techniques for parallel programs . In Automatic program construction techniques . Macmillan , 1984 . Patrick Cousot and Radhia Cousot. Invariance proof methods and analysis techniques for parallel programs. In Automatic program construction techniques. Macmillan, 1984."},{"key":"e_1_3_2_1_18_1","volume-title":"CAV","volume":"6806","author":"Donaldson Alastair","year":"2011","unstructured":"Alastair Donaldson , Alexander Kaiser , Daniel Kroening , and Thomas Wahl . Symmetry-aware predicate abstraction for shared-variable concurrent programs . In CAV , volume 6806 , 2011 . Alastair Donaldson, Alexander Kaiser, Daniel Kroening, and Thomas Wahl. Symmetry-aware predicate abstraction for shared-variable concurrent programs. In CAV, volume 6806, 2011."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0155-3"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_22"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806613"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103693"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429086"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535885"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677012"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935310"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/645396.651955"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.12.006"},{"key":"e_1_3_2_1_29_1","volume-title":"Backward reachability of arraybased systems by SMT solving: Termination and invariant synthesis. Logical Methods in Computer Science, 6(4)","author":"Ghilardi Silvio","year":"2010","unstructured":"Silvio Ghilardi and Silvio Ranise . Backward reachability of arraybased systems by SMT solving: Termination and invariant synthesis. Logical Methods in Computer Science, 6(4) , 2010 . Silvio Ghilardi and Silvio Ranise. Backward reachability of arraybased systems by SMT solving: Termination and invariant synthesis. Logical Methods in Computer Science, 6(4), 2010."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254112"},{"key":"e_1_3_2_1_31_1","volume-title":"CAV","author":"Gupta Ashutosh","year":"2011","unstructured":"Ashutosh Gupta , Corneliu Popeea , and Andrey Rybalchenko . Threader : A constraint-based verifier for multi-threaded programs . In CAV , 2011 . Ashutosh Gupta, Corneliu Popeea, and Andrey Rybalchenko. Threader: A constraint-based verifier for multi-threaded programs. In CAV, 2011."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950330"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/996841.996844"},{"key":"e_1_3_2_1_34_1","volume-title":"CAV","author":"Henzinger Thomas A.","year":"2003","unstructured":"Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , and Shaz Qadeer . Thread-modular abstraction refinement . In CAV , 2003 . Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Shaz Qadeer. Thread-modular abstraction refinement. In CAV, 2003."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.169.6"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_6"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/69575.69577"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44584-6_11"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11319-2_18"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1977.229904"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/11921240_13"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.5555\/2391451.2391467"},{"key":"e_1_3_2_1_44_1","volume-title":"SAS","author":"Monniaux David","year":"2016","unstructured":"David Monniaux and Laure Gonnord . Cell morphing : From array programs to array-free horn clauses . In SAS , 2016 . David Monniaux and Laure Gonnord. Cell morphing: From array programs to array-free horn clauses. In SAS, 2016."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.5555\/1763048.1763080"},{"key":"e_1_3_2_1_46_1","volume-title":"IPDPS","author":"Nieto Leonor Prensa","year":"2001","unstructured":"Leonor Prensa Nieto . Completeness of the Owicki-Gries system for parameterized parallel programs . In IPDPS , 2001 . Leonor Prensa Nieto. Completeness of the Owicki-Gries system for parameterized parallel programs. In IPDPS, 2001."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.5555\/646485.694452"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.5555\/28907"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-015-0222-5"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33125-1_12"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10672-9_5"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.5555\/646735.701607"}],"event":{"name":"POPL '17: The 44th Annual ACM SIGPLAN Symposium on Principles of Programming Languages","location":"Paris France","acronym":"POPL '17","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3009837.3009893","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3009837.3009893","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T15:05:34Z","timestamp":1750259134000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3009837.3009893"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1]]},"references-count":51,"alternative-id":["10.1145\/3009837.3009893","10.1145\/3009837"],"URL":"https:\/\/doi.org\/10.1145\/3009837.3009893","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3093333.3009893","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2017,1]]},"assertion":[{"value":"2017-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}