{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:42:35Z","timestamp":1780994555510,"version":"3.54.1"},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"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":[[2025,1,7]]},"abstract":"<jats:p>\n                    Although there have been many approaches for developing formal memory models that support integerpointer casts, previous approaches share the drawback that they are not designed for\n                    <jats:italic toggle=\"yes\">end-to-end<\/jats:italic>\n                    <jats:italic toggle=\"yes\">verification<\/jats:italic>\n                    ,failing to support some important source-level coding patterns, justify some backend optimizations, or lack a source-level logic for program verification.\n                  <\/jats:p>\n                  <jats:p>This paper presents Archmage, a framework for integer-pointer casting designed for end-to-end verification,supporting a wide range of source-level coding patterns, backend optimizations, and a formal notion of out-ofmemory. To facilitate end-to-end verification via Archmage, we also present two systems based on Archmage: CompCertCast, an extension of CompCert with Archmage to bring a full verified compilation chain to integer-pointer casting programs, and Archmage logic, a source-level logic for reasoning about integerpointer casts. We design CompCertCast such that the overhead from formally supporting integer-pointer casts is mitigated, and illustrate the effectiveness of Archmage logic by verifying an xor-based linked-list implementation, Together, our paper presents the first practical end-to-end verification chain for programs containing integer-pointer casts.<\/jats:p>","DOI":"10.1145\/3704881","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"1326-1354","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer Casting"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-9834-5352","authenticated-orcid":false,"given":"Yonghyun","family":"Kim","sequence":"first","affiliation":[{"name":"Seoul National University, Seoul, South Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6684-0921","authenticated-orcid":false,"given":"Minki","family":"Cho","sequence":"additional","affiliation":[{"name":"Seoul National University, Seoul, South Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-6423-9561","authenticated-orcid":false,"given":"Jaehyung","family":"Lee","sequence":"additional","affiliation":[{"name":"Seoul National University, Seoul, South Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3897-1828","authenticated-orcid":false,"given":"Jinwoo","family":"Kim","sequence":"additional","affiliation":[{"name":"Seoul National University, Seoul, South Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-0035-4077","authenticated-orcid":false,"given":"Taeyoung","family":"Yoon","sequence":"additional","affiliation":[{"name":"Seoul National University, Seoul, South Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7093-3824","authenticated-orcid":false,"given":"Youngju","family":"Song","sequence":"additional","affiliation":[{"name":"MPI-SWS, Saarbrucken, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1656-0913","authenticated-orcid":false,"given":"Chung-Kil","family":"Hur","sequence":"additional","affiliation":[{"name":"Seoul National University, Seoul, South Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107256552"},{"key":"e_1_3_2_3_1","unstructured":"Andrew W. Appel Lennart Beringer Qinxiang Cao and Josiah Dodds. 2023. Verifiable C. Vol. 1. https:\/\/raw.githubusercontent.com\/PrincetonUniversity\/VST\/master\/doc\/VC.pdf"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2579080"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-12736-1_24"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_5"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9496-y"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040327"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_4"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/115372.115320"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738005"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.13939050"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2004.1281665"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276495"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498681"},{"key":"e_1_3_2_18_1","article-title":"Formal Certification of a Compiler Back-end or: Programming a Compiler with a Proof Assistant","author":"Leroy Xavier","year":"2006","unstructured":"Xavier Leroy . 2006. Formal Certification of a Compiler Back-end or: Programming a Compiler with a Proof Assistant. In Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2006).","journal-title":"Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632848"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290380"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571220"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371091"},{"key":"e_1_3_2_25_1","first-page":"31","article-title":"Conditional Contextual Refinement","author":"Song Youngju","year":"2023","unstructured":"Youngju Song, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Sammler, and Derek Dreyer. 2023. Conditional Contextual Refinement. Proc. ACM Program. Lang. 7, POPL, Article 39 (jan 2023), 31 pages. https:\/\/doi.org\/10.1145\/3571232","journal-title":"Proc. ACM Program. Lang. 7, POPL"},{"key":"e_1_3_2_26_1","unstructured":"The Coq Development Team. 2021. The Coq Proof Assistant 8.13.2 Reference Manual. https:\/\/coq.github.io\/doc\/V8.13.2\/refman\/."},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290375"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371119"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704881","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704881","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:14:05Z","timestamp":1770200045000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704881"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":27,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704881"],"URL":"https:\/\/doi.org\/10.1145\/3704881","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}