{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T14:15:50Z","timestamp":1784211350758,"version":"3.55.0"},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T00:00:00Z","timestamp":1767830400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"crossref","award":["503812980"],"award-info":[{"award-number":["503812980"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,1,8]]},"abstract":"<jats:p>\n                    Implementation bugs threaten the soundness of algorithmic software verifiers. Generating correctness certificates for correct programs allows for efficient independent validation of verification results, and thus helps to reveal such bugs. Automatic generation of small, compact correctness proofs for concurrent programs is challenging, as the correctness arguments may depend on the particular interleaving, which can lead to exponential explosion. We present an approach that converts an interleaving-based correctness proof, as generated by many algorithmic verifiers, into a thread-modular correctness proof in the style of Owicki and Gries. We automatically synthesize\n                    <jats:italic toggle=\"yes\">ghost variables<\/jats:italic>\n                    that capture the relevant interleaving information, and abstract away irrelevant details. Our evaluation shows that the approach is efficient in practice and generates compact proofs, compared to a baseline.\n                  <\/jats:p>","DOI":"10.1145\/3776684","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"1212-1240","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5656-306X","authenticated-orcid":false,"given":"Frank","family":"Sch\u00fcssele","sequence":"first","affiliation":[{"name":"University of Freiburg, Freiburg im Breisgau, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-3696-6269","authenticated-orcid":false,"given":"Matthias","family":"Zumkeller","sequence":"additional","affiliation":[{"name":"University of Freiburg, Freiburg im Breisgau, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-9482-3900","authenticated-orcid":false,"given":"Miriam","family":"Lagunes-Rochin","sequence":"additional","affiliation":[{"name":"University of Freiburg, Freiburg im Breisgau, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4885-0728","authenticated-orcid":false,"given":"Dominik","family":"Klumpp","sequence":"additional","affiliation":[{"name":"LIX - CNRS - \u00c9cole Polytechnique, Palaiseau, France"},{"name":"University of Freiburg, Freiburg im Breisgau, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-745-5"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-66149-5_11"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45139-0_7"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10009-017-0469-Y"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-22308-2_8"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-90660-2_9"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.TCS.2006.12.034"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/2984450.2984457"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48899-7_17"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","unstructured":"Agostino Cortesi Giulia Costantini and Pietro Ferrara. 2013. A Survey on Product Operators in Abstract Interpretation. In Semantics Abstract Interpretation and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday Manhattan Kansas USA 19-20th September 2013 (EPTCS Vol. 129) Anindya Banerjee Olivier Danvy Kyung-Goo Doh and John Hatcliff (Eds.). 325\u2013336. doi:10.4204\/EPTCS.129.19","DOI":"10.4204\/EPTCS.129.19"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-67067-2_9"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-82700-6_4"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1609\/icaps.v27i1.13818"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535885"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523727"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371081"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-63498-7_17"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","unstructured":"Nils Froleyks Emily Yu Mathias Preiner Armin Biere and Keijo Heljanko. 2025. Introducing Certificates to the Hardware Model Checking Competition. 15931 (2025) 281\u2013295. doi:10.1007\/978-3-031-98668-0_14","DOI":"10.1007\/978-3-031-98668-0_14"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63166-6_10"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254112"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926424"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950330"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03237-0_7"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-50521-8_1"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009893"},{"key":"e_1_3_2_29_2","unstructured":"Jochen Hoenicke and Tanja Schindler. 2022. A Simple Proof Format for SMT. In Proceedings of the 20th Internal Workshop on Satisfiability Modulo Theories co-located with the 11th International foint Conference on Automated Reasoning (IfCAR 2022) part of the 8th Federated Logic Conference (FLoC 2022) Haifa Israel August 11-12 2022 (CEUR Workshop Proceedings Vol. 3185) David D\u00e9harbe and Antti E. J. Hyv\u00e4rinen (Eds.). ceur-ws.org 54\u201370. https:\/\/ceur-ws.org\/Vol-3185\/paper9527.pdf"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","unstructured":"Hossein Hojjat Philipp R\u00fcmmer Pavle Subotic and Wang Yi. 2014. Horn Clauses for Communicating Timed Systems. In Proceedings First Workshop on Horn Clauses for Verification and Synthesis HCVS 2014 Vienna Austria 17 July 2014 (EPTCS Vol. 169) Nikolaj S. Bj\u00f8rner Fabio Fioravanti Andrey Rybalchenko and Valerio Senni (Eds.). 39\u201352. doi:10.4204\/EPTCS.169.6","DOI":"10.4204\/EPTCS.169.6"},{"key":"e_1_3_2_31_2","volume-title":"Developing methods for computer programs including a notion of interference. Ph. D. Dissertation","author":"Jones Cliff B.","year":"1981","unstructured":"Cliff B. Jones. 1981. Developing methods for computer programs including a notion of interference. Ph. D. Dissertation. University of Oxford, UK. https:\/\/ethos.bl.uk\/OrderDetails.do?uin=uk.bl.ethos.259064"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1977.229904"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56496-9_14"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_14"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(1:26)2012"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54013-4_3"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-52234-0_21"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS.2001.925138"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-28644-8_4"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/800113.803634"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360224"},{"key":"e_1_3_2_42_2","volume-title":"Introduction to static analysis: an abstract interpretation perspective","author":"Rival Xavier","year":"2020","unstructured":"Xavier Rival and Kwangkeun Yi. 2020. Introduction to static analysis: an abstract interpretation perspective. MIT Press."},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30820-8_34"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","unstructured":"Hans-J\u00f6rg Schurr Mathias Fleury Haniel Barbosa and Pascal Fontaine. 2021. Alethe: Towards a Generic SMT Proof Format (extended abstract). In Proceedings Seventh Workshop on Proof eXchange for Theorem Proving PxTP 2021 Pittsburg PA USA July 11 2021 (EPTCS Vol. 336) Chantal Keller and Mathias Fleury (Eds.). 49\u201354. doi:10.4204\/EPTCS.336.6","DOI":"10.4204\/EPTCS.336.6"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57256-2_31"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","unstructured":"Frank Sch\u00fcssele Matthias Zumkeller Miriam Lagunes-Rochin and Dominik Klumpp. 2025. The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs (Extended Version). Technical Report. doi:10.48550\/arXiv.2511.20369","DOI":"10.48550\/arXiv.2511.20369"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","unstructured":"Frank Sch\u00fcssele Matthias Zumkeller Miriam Lagunes-Rochin and Dominik Klumpp. 2026. Artifact for the POPL\u20192026 Paper \"The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs\". doi:10.5281\/zenodo.17347697","DOI":"10.5281\/zenodo.17347697"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/2970276.2970337"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679412"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-09284-3_31"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776684","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T13:42:25Z","timestamp":1784209345000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776684"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":49,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776684"],"URL":"https:\/\/doi.org\/10.1145\/3776684","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}