{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T14:58:23Z","timestamp":1787065103878,"version":"build-2736575974"},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>Iris is a generic separation logic framework that has been instantiated to reason about a wide range of programming languages and language features. Most Iris instances are defined on simple core calculi, but by connecting Iris to new or existing formal semantics for practical languages, we can also use it to reason about real programs. In this paper we develop an Iris instance based on CompCert, the verified C compiler, allowing us to prove correctness of C programs under the same semantics we use to compile and run them. We take inspiration from the Verified Software Toolchain (VST), a prior separation logic for CompCert C, and reimplement the program logic of VST in Iris. Unlike most Iris instances, this involves both a new model of resources for CompCert memories, and a new definition of weakest preconditions\/Hoare triples, as the Iris defaults for both of these cannot be applied to CompCert as is. Ultimately, we obtain a complete program logic for CompCert C within Iris, and we reconstruct enough of VST\u2019s top-level automation to prove correctness of simple C programs.<\/jats:p>","DOI":"10.1145\/3632848","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T15:48:51Z","timestamp":1704469731000},"page":"148-174","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["An Iris Instance for Verifying CompCert C Programs"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5351-895X","authenticated-orcid":false,"given":"William","family":"Mansky","sequence":"first","affiliation":[{"name":"University of Illinois Chicago, Chicago, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-2465-1082","authenticated-orcid":false,"given":"Ke","family":"Du","sequence":"additional","affiliation":[{"name":"University of Illinois Chicago, Chicago, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","unstructured":"Anonymous. 2023. VST on Iris. https:\/\/doi.org\/10.5281\/zenodo.8423866 10.5281\/zenodo.8423866","DOI":"10.5281\/zenodo.8423866"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107256552"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/2831143.2831157"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290378"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06410-9_9"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9457-5"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359632"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","unstructured":"The Coq Development Team. 2023. The Coq Proof Assistant. https:\/\/doi.org\/10.5281\/zenodo.8161141 10.5281\/zenodo.8161141","DOI":"10.5281\/zenodo.8161141"},{"key":"e_1_3_1_10_1","volume-title":"Compiler Correctness for Concurrency: from concurrent separation logic to shared-memory assembly language","author":"Cuellar Santiago","year":"2020","unstructured":"Santiago Cuellar, Nick Giannarakis, Jean-Marie Madiot, William Mansky, Lennart Beringer, Qinxiang Cao, and Andrew Appel. 2020. Compiler Correctness for Concurrency: from concurrent separation logic to shared-memory assembly language. Technical Report. Princeton University."},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371102"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","unstructured":"Robert Dockins Aquinas Hobor and Andrew W. Appel. 2009. A Fresh Look at Separation Algebras and Share Accounting. In Programming Languages and Systems 7th Asian Symposium APLAS 2009 Seoul Korea December 14-16 2009. Proceedings. 161\u2013177. https:\/\/doi.org\/10.1007\/978-3-642-10672-9_13 10.1007\/978-3-642-10672-9_13","DOI":"10.1007\/978-3-642-10672-9_13"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-17(3:9)2021"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-76637-7_3"},{"key":"e_1_3_1_15_1","doi-asserted-by":"crossref","unstructured":"Arma\u00ebl Gu\u00e9neau Johannes Hostert Simon Spies Michael Sammler Lars Birkedal and Derek Dreyer. 2023. Melocoton: A Program Logic for Verified Interoperability Between OCaml and C. (May 2023). unpublished draft.","DOI":"10.1145\/3622823"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792878.1792914"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314595"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_1_22_1","unstructured":"Jan-Oliver Kaiser Hoang-Hai Dang Derek Dreyer Ori Lahav and Viktor Vafeiadis. 2017. Strong Logic for Weak Memory: Reasoning About Release-Acquire Consistency in Iris. In ECOOP\u201917: 31st European Conference on Object-Oriented Programming (LIPIcs Vol. 74). 17:1\u201317:29."},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294106"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236772"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_13"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_22"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_1_28_1","volume-title":"The CompCert Memory Model, Version 2","author":"Leroy Xavier","year":"2012","unstructured":"Xavier Leroy, Andrew W. Appel, Sandrine Blazy, and Gordon Stewart. 2012. The CompCert Memory Model, Version 2. Research report RR-7987. INRIA. http:\/\/hal.inria.fr\/hal-00703441"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","unstructured":"William Mansky. 2022. Bringing Iris into the Verified Software Toolchain. CoRR abs\/2207.06574 (2022). https:\/\/doi.org\/10.48550\/ARXIV.2207.06574 10.48550\/ARXIV.2207.06574","DOI":"10.48550\/ARXIV.2207.06574"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133911"},{"key":"e_1_3_1_31_1","doi-asserted-by":"crossref","first-page":"428","DOI":"10.1007\/978-3-030-44914-8_16","volume-title":"Programming Languages and Systems","author":"Mansky William","year":"2020","unstructured":"William Mansky, Wolf Honor\u00e9, and Andrew W. Appel. 2020. Connecting Higher-Order Separation Logic to a First-Order Outside World. In Programming Languages and Systems, Peter M\u00fcller (Ed.). Springer International Publishing, Cham, 428\u2013455."},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523432"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591265"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571220"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454031"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547631"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487248"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-90870-6_4"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2021.32"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632848","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632848","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T16:05:41Z","timestamp":1751645141000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632848"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":39,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632848"],"URL":"https:\/\/doi.org\/10.1145\/3632848","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}