{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T20:49:15Z","timestamp":1770238155384,"version":"3.49.0"},"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\/"}],"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>\n                    The Rust programming language continues to rise in popularity, and as such, warrants the close attention of the programming languages community. In this work, we present a new foundational contribution towards the theoretical understanding of Rust\u2019s semantics. We prove that LLBC, a high-level, borrow-centric model previously proposed for Rust\u2019s semantics and execution, is sound with regards to a low-level pointer-based language\n                    <jats:italic toggle=\"yes\">\u00e0 la<\/jats:italic>\n                    CompCert. Specifically, we prove the following: that LLBC is a correct view over a traditional model of execution; that LLBC\u2019s symbolic semantics are a correct abstraction of LLBC programs; and that LLBC\u2019s symbolic semantics act as a borrow-checker for LLBC, i.e. that symbolically-checked LLBC programs do not get stuck when executed on a heap-and-addresses model of execution.\n                  <\/jats:p>\n                  <jats:p>To prove these results, we introduce a new proof style that considerably simplifies our proofs of simulation, which relies on a notion of hybrid states. Equipped with this reasoning framework, we show that a new addition to LLBC\u2019s symbolic semantics, namely a join operation, preserves the abstraction and borrow-checking properties. This in turn allows us to add support for loops to the Aeneas framework; we show, using a series of examples and case studies, that this unlocks new expressive power for Aeneas.<\/jats:p>","DOI":"10.1145\/3674640","type":"journal-article","created":{"date-parts":[[2024,8,15]],"date-time":"2024-08-15T12:49:04Z","timestamp":1723726144000},"page":"426-454","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Sound Borrow-Checking for Rust via Symbolic Semantics"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3297-9156","authenticated-orcid":false,"given":"Son","family":"Ho","sequence":"first","affiliation":[{"name":"Inria, Paris, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2642-543X","authenticated-orcid":false,"given":"Aymeric","family":"Fromherz","sequence":"additional","affiliation":[{"name":"Inria, Paris, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7347-3050","authenticated-orcid":false,"given":"Jonathan","family":"Protzenko","sequence":"additional","affiliation":[{"name":"Microsoft Azure Research, Redmond, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,8,15]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360573"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837022"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_22"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/872752.873511"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-17524-9_1"},{"key":"e_1_3_1_7_1","doi-asserted-by":"crossref","unstructured":"Cristiano Calcagno Dino Distefano Peter O\u2019Hearn and Hongseok Yang. 2009. Compositional shape analysis by means of bi-abduction. In Proceedings of the 36th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). 289\u2013300.","DOI":"10.1145\/1480881.1480917"},{"key":"e_1_3_1_8_1","unstructured":"Bor-Yuh Evan Chang and Xavier Rival. 2008. Relational inductive shape analysis. In Proceedings of the ACM Symposium on Principles of Programming Languages (POPL)."},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_1_10_1","unstructured":"Xavier Denis Jacques-Henri Jourdan and Claude March\u00e9. 2021. The Creusot Environment for the Deductive Verification of Rust Programs. Research Report RR-9448. Inria Saclay - \u00cele de France. https:\/\/hal.inria.fr\/hal-03526634"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17244-1_6"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_19"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","unstructured":"Son Ho Aymeric Fromherz and Jonathan Protzenko. 2024a. Artifact for: Sound Borrow-Checking for Rust via Symbolic Semantics. https:\/\/doi.org\/10.5281\/zenodo.11500453 10.5281\/zenodo.11500453","DOI":"10.5281\/zenodo.11500453"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","unstructured":"Son Ho Aymeric Fromherz and Jonathan Protzenko. 2024b. Sound Borrow-Checking for Rust via Symbolic Semantics (Long Version). https:\/\/doi.org\/10.48550\/arXiv.2404.02680 10.48550\/arXiv.2404.02680 arXiv:2404.02680 [cs.PL]","DOI":"10.48550\/arXiv.2404.02680"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547647"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","unstructured":"Marieke Huisman and Bart Jacobs. 2000. Java Program Verification via a Hoare Logic with Abrupt Termination Vol. 1783. 284-303. https:\/\/doi.org\/10.1007\/3-540-46428-X_20 10.1007\/3-540-46428-X_20","DOI":"10.1007\/3-540-46428-X_20"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-57288-8_15"},{"key":"e_1_3_1_18_1","first-page":"1","article-title":"Stacked borrows: an aliasing model for Rust","volume":"4","author":"Jung Ralf","year":"2019","unstructured":"Ralf Jung, Hoang-Hai Dang, Jeehoon Kang, and Derek Dreyer. 2019. Stacked borrows: an aliasing model for Rust. Proceedings of the ACMon Programming Languages 4, POPL (2019), 1-32.","journal-title":"Proceedings of the ACMon Programming Languages"},{"key":"e_1_3_1_19_1","first-page":"1","article-title":"RustBelt: Securing the foundations of the Rust programming language","volume":"2","author":"Jung Ralf","year":"2017","unstructured":"Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. 2017. RustBelt: Securing the foundations of the Rust programming language. Proceedings of the ACMon Programming Languages 2, POPL (2017), 1-34.","journal-title":"Proceedings of the ACMon Programming Languages"},{"key":"e_1_3_1_20_1","unstructured":"Franziskus Kiefer and Lucas Franceschino. 2023. Introducing hax. https:\/\/hacspec.org\/blog\/posts\/hax-v0-1\/."},{"key":"e_1_3_1_21_1","doi-asserted-by":"crossref","unstructured":"Andrea Lattuada Travis Hance Chanhee Cho Matthias Brun Isitha Subasinghe Yi Zhou Jon Howell Bryan Parno and Chris Hawblitzel. 2023. Verus: Verifying Rust Programs using Linear Ghost Types. In Proceedings of the ACM Conference on Object-Oriented Programming Systems Languages and Applications (OOPSLA).","DOI":"10.1145\/3586037"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_21"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_5"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_1_25_1","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_26_1","doi-asserted-by":"crossref","unstructured":"Yusuke Matsushita Xavier Denis Jacques-Henri Jourdan and Derek Dreyer. 2022. RustHorn-Belt: A semantic foundation for functional verification of Rust programs with unsafe code. In Proceedings of the 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI).","DOI":"10.1145\/3519939.3523704"},{"key":"e_1_3_1_27_1","doi-asserted-by":"crossref","unstructured":"Yusuke Matsushita Takeshi Tsukada and Naoki Kobayashi. 2020. RustHorn: CHC-Based Verification for Rust Programs.. In ESOP. 484\u2013514.","DOI":"10.1007\/978-3-030-44914-8_18"},{"key":"e_1_3_1_28_1","unstructured":"The Miri Team. 2021. Miri. https:\/\/github.com\/rust-lang\/miri\/."},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_26"},{"key":"e_1_3_1_31_1","unstructured":"National Security Agency. 2022. Software Memory Safety. https:\/\/media.defense.gov\/2022\/Nov\/10\/2003112742\/-1\/-1\/0\/CSI_SOFTWARE_MEMORY_SAFETY.PDF."},{"key":"e_1_3_1_32_1","unstructured":"Michael Norrish. 1998. C formalised in HOL. (1998)."},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_23"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2544174.2500598"},{"key":"e_1_3_1_36_1","unstructured":"Jonathan Protzenko. 2014. Mezzo: a typed language for safe effectful concurrent programs. Ph. D. Dissertation. Universit\u00e9 Paris Diderot-Paris 7."},{"key":"e_1_3_1_37_1","unstructured":"StackOverflow. 2023. 2023 Developer Survey. https:\/\/survey.stackoverflow.co\/2023\/#section-admired-and-desired-programming-scripting-and-markup-languages."},{"key":"e_1_3_1_38_1","doi-asserted-by":"crossref","unstructured":"Nikhil Swamy C\u00e2t\u00e2lin Hri\u0163cu Chantal Keller Aseem Rastogi Antoine Delignat-Lavaud Simon Forest Karthikeyan Bhargavan C\u00e9dric Fournet Pierre-Yves Strub Markulf Kohlweiss et al. 2016. Dependent types and multi-monadic effects in F. In Proceedings of the ACM Symposium on Principles of Programming Languages (POPL). 256-270.","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_3_1_39_1","unstructured":"The Register. 2022. In Rust We Trust: Microsoft Azure CTO shuns C and C++. https:\/\/www.theregister.com\/2022\/09\/20\/rust_microsoft_c\/."},{"key":"e_1_3_1_40_1","unstructured":"The Rust Compiler Team. 2021. The Polonius Book. https:\/\/rust-lang.github.io\/polonius\/."},{"key":"e_1_3_1_41_1","unstructured":"The Rust Compiler Team. 2024. Guide to rustc development. https:\/\/rustc-dev-guide.rust-lang.org\/borrow_check\/two_phase_borrows.html."},{"key":"e_1_3_1_42_1","unstructured":"Neven Villani. 2023. Tree Borrows a new aliasing model for Rust. https:\/\/perso.crans.org\/vanille\/treebor\/."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3674640","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3674640","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T07:49:13Z","timestamp":1770191353000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3674640"}},"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\/3674640"],"URL":"https:\/\/doi.org\/10.1145\/3674640","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"}}]}}