{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:41:19Z","timestamp":1780994479889,"version":"3.54.1"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2024,8,15]],"date-time":"2024-08-15T00:00:00Z","timestamp":1723680000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["2247088"],"award-info":[{"award-number":["2247088"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,8,15]]},"abstract":"<jats:p>This paper provides a novel approach to reconciling complex low-level memory model features, such as pointerinteger casts, with desired refinements that are needed to justify the correctness of program transformations. The idea is to use a \u201ctwo-phase\u201d memory model, one with an unbounded memory and corresponding unbounded integer type, and one with a finite memory; the connection between the two levels is made explicit by a notion of refinement that handles out-of-memory behaviors. This approach allows for more optimizations to be performed and establishes a clear boundary between the idealized semantics of a program and the implementation of that program on finite hardware.<\/jats:p>\n                  <jats:p>The two-phase memory model has been incorporated into an LLVM IR semantics, demonstrating its utility in practice in the context of a low-level language with features like undef and bitcast. This yields infinite and finite memory versions of the language semantics that are proven to be in refinement with respect to out-of-memory behaviors. Each semantics is accompanied by a verified executable reference interpreter. The semantics justify optimizations, such as dead-alloca-elimination, that were previously impossible or difficult to prove correct.<\/jats:p>","DOI":"10.1145\/3674652","type":"journal-article","created":{"date-parts":[[2024,8,15]],"date-time":"2024-08-15T12:49:04Z","timestamp":1723726144000},"page":"789-817","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["A Two-Phase Infinite\/Finite Low-Level Memory Model: Reconciling Integer\u2013Pointer Casts, Finite Space, and undef at the LLVM IR Level of Abstraction"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3469-7219","authenticated-orcid":false,"given":"Calvin","family":"Beck","sequence":"first","affiliation":[{"name":"University of Pennsylvania, Philadelphia, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3388-1257","authenticated-orcid":false,"given":"Irene","family":"Yoon","sequence":"additional","affiliation":[{"name":"Inria, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-4486-7222","authenticated-orcid":false,"given":"Hanxi","family":"Chen","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4585-6470","authenticated-orcid":false,"given":"Yannick","family":"Zakowski","sequence":"additional","affiliation":[{"name":"Inria - ENS de Lyon - CNRS - UCBL1 - LIP - UMR 5668, Lyon, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3516-1512","authenticated-orcid":false,"given":"Steve","family":"Zdancewic","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,8,15]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","unstructured":"CalvinBeck IreneYoon HanxiChen YannickZakowski andSteveZdancewic. 2024. A Two-Phase Infinite\/Finite Low-Level Memory Model. https:\/\/doi.org\/10.5281\/zenodo.1251880010.5281\/zenodo.12518800","DOI":"10.5281\/zenodo.12518800"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-12736-1_24"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_5"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9496-y"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9439-z"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535876"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290357"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.5555\/3049832.3049844"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_3"},{"key":"e_1_3_1_12_2","unstructured":"RaymondChen.2014.Undefined behavior can result in time travel (among other things but time travel is the funkiest).https:\/\/devblogs.microsoft.com\/oldnewthing\/20140627-00\/?p=633"},{"key":"e_1_3_1_13_2","first-page":"126","article-title":"QuickChick: Property-based testing for Coq","volume":"125","author":"D\u00e9n\u00e8s Maxime","year":"2014","unstructured":"MaximeD\u00e9n\u00e8s,CatalinHritcu,LeonidasLampropoulos,ZoeParaskevopoulou, andBenjamin CPierce.2014.QuickChick: Property-based testing for Coq. InThe Coq Workshop, Vol.125.126.","journal-title":"The Coq Workshop"},{"key":"e_1_3_1_14_2","volume-title":"A Formal Semantics of C with Applications","author":"Ellison Charles","year":"2012","unstructured":"CharlesEllison. 2012. A Formal Semantics of C with Applications. Ph. D. Dissertation. University of Illinois. 2142\/34297"},{"key":"e_1_3_1_15_2","unstructured":"ISO 9899:1999 1999.Programming Languages \u2014 C.Standard. International Organization for Standardization."},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009850"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738005"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_4"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08970-6_36"},{"key":"e_1_3_1_22_2","unstructured":"Robbert JanKrebbers.2015.TheCstandard formalizedin Coq.Ph. D. Dissertation. [Sl]:[Sn].2066\/147182"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3276495"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3140587.3062343"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386010"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498681"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9099-0"},{"key":"e_1_3_1_28_2","volume-title":"ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress","author":"Leroy Xavier","year":"2016","unstructured":"XavierLeroy,SandrineBlazy,DanielK\u00e4stner,BernhardSchommer,MarkusPister, andChristianFerdinand.2016.CompCert - A Formally Verified Optimizing Compiler. InERTS 2016: Embedded Real Time Software and Systems, 8th European Congress.SEE, Toulouse,France.https:\/\/inria.hal.science\/hal-01238879"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.7"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454030"},{"key":"e_1_3_1_31_2","unstructured":"AlanaMarzoev.2022.How much does Rust\u2019s bounds checking actually cost? \u2014 blog.readyset.io.https:\/\/blog.readyset.io\/bounds-checks\/. [Accessed 27-02-2024]."},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290380"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908081"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2010.03.012"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487248"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/1925844.1926393"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371119"},{"key":"e_1_3_1_38_2","volume-title":"Modular Semantics and Metatheory for LLVM IR","author":"Yoon Euisun","year":"2023","unstructured":"EuisunYoon.2023.Modular Semantics and Metatheory for LLVM IR.Ph. D. Dissertation.University of Pennsylvania. https:\/\/doi.org\/20.500.14332\/59534 20.500.14332\/59534"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/3547630"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/3473572"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-63618-0_3"},{"key":"e_1_3_1_42_2","unstructured":"SteveZdancewicet al. [n. d.]. Vellvm. https:\/\/github.com\/vellvm\/vellvm"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3674652","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3674652","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T07:50:15Z","timestamp":1770191415000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3674652"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,8,15]]},"references-count":41,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2024,8,15]]}},"alternative-id":["10.1145\/3674652"],"URL":"https:\/\/doi.org\/10.1145\/3674652","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,8,15]]},"assertion":[{"value":"2024-02-28","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-06-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-15","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}