{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,8]],"date-time":"2026-10-08T11:33:37Z","timestamp":1791459217026,"version":"4.3.4"},"reference-count":67,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T00:00:00Z","timestamp":1570665600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001711","name":"Schweizerischer Nationalfonds zur F\u00f6rderung der Wissenschaftlichen Forschung","doi-asserted-by":"crossref","award":["200021_169503"],"award-info":[{"award-number":["200021_169503"]}],"id":[{"id":"10.13039\/501100001711","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":[[2019,10,10]]},"abstract":"<jats:p>Rust's type system ensures memory safety: well-typed Rust programs are guaranteed to not exhibit problems such as dangling pointers, data races, and unexpected side effects through aliased references. Ensuring correctness properties beyond memory safety, for instance, the guaranteed absence of assertion failures or more-general functional correctness, requires static program verification. For traditional system programming languages, formal verification is notoriously difficult and requires complex specifications and logics to reason about pointers, aliasing, and side effects on mutable state. This complexity is a major obstacle to the more-widespread verification of system software.<\/jats:p>\n                  <jats:p>\n                    In this paper, we present a novel verification technique that leverages Rust's type system to greatly simplify the specification and verification of system software written in Rust. We analyse information from the Rust compiler and synthesise a corresponding\n                    <jats:italic>core proof<\/jats:italic>\n                    for the program in a flavour of separation logic tailored to automation. To verify correctness properties beyond memory safety, users can annotate Rust programs with specifications at the abstraction level of Rust expressions; our technique weaves them into the core proof to verify modularly whether these specifications hold. Crucially, our proofs are constructed and checked automatically without exposing the underlying formal logic, allowing users to work exclusively at the level of abstraction of the programming language. As such, our work enables a new kind of verification tool, with the potential to impact a wide audience and allow the Rust community to benefit from state-of-the-art verification techniques. We have implemented our techniques for a subset of Rust; our evaluation on several thousand functions from widely-used Rust crates demonstrates its effectiveness.\n                  <\/jats:p>","DOI":"10.1145\/3360573","type":"journal-article","created":{"date-parts":[[2019,10,11]],"date-time":"2019-10-11T10:53:33Z","timestamp":1570791213000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":124,"title":["Leveraging rust types for modular specification and verification"],"prefix":"10.1145","volume":"3","author":[{"given":"Vytautas","family":"Astrauskas","sequence":"first","affiliation":[{"name":"ETH Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Federico","family":"Poli","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alexander J.","family":"Summers","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,10,10]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Logic in Computer Science (LICS)","author":"Abadi Mart\u00ecn"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.3363914"},{"key":"e_1_2_2_3_1","volume-title":"Summers","author":"Astrauskas Vytautas","year":"2019"},{"key":"e_1_2_2_4_1","volume-title":"Verification, Model Checking, and Abstract Interpretation (VMCAI) (Lecture Notes in Computer Science) , Barbara Jobstmann and K","author":"Bakst Alexander"},{"key":"e_1_2_2_5_1","volume-title":"Automated Technology for Verification and Analysis (ATVA) (Lecture Notes in Computer Science) , Shuvendu K","author":"Baranowski Marek"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1953122.1953145"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048237.2048242"},{"key":"e_1_2_2_8_1","volume-title":"Checking Interference with Fractional Permissions. In Static Analysis Symposium (SAS) (Lecture Notes in Computer Science) , Radhia Cousot (Ed.)","volume":"2694","author":"Boyland John","year":"2003"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45337-7_2"},{"key":"e_1_2_2_10_1","volume-title":"Fast Actors. In International Workshop on Programming Based on Actors, Agents, and Decentralized Control (AGERE!","author":"Clebsch Sylvan","year":"2015"},{"key":"e_1_2_2_11_1","volume-title":"https:\/\/github.com\/rust-lang\/rust-clippy Accessed","author":"Clippy Clippy","year":"2019"},{"key":"e_1_2_2_12_1","volume-title":"VCC: A Practical System for Verifying Concurrent C. In Theorem Proving in Higher Order Logics (TPHOLs) (Lecture Notes in Computer Science)","author":"Cohen Ernie","year":"2009"},{"key":"e_1_2_2_13_1","unstructured":"Coq Team. 2014. The Coq Proof Assistant Reference Manual. http:\/\/coq.inria.fr .  Coq Team. 2014. The Coq Proof Assistant Reference Manual. http:\/\/coq.inria.fr ."},{"key":"e_1_2_2_14_1","volume-title":"Programming Language Design and Implementation (PLDI) , Barbara G","author":"Crary Karl"},{"key":"e_1_2_2_15_1","volume-title":"Automated Deduction (CADE) (Lecture Notes in Computer Science), Amy P","author":"de Moura Leonardo Mendon\u00e7a"},{"key":"e_1_2_2_16_1","volume-title":"Sandrine Blazy and Marsha Chechik (Eds.)","volume":"9971","author":"Dockins Robert","year":"2016"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1047659.1040325"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2398857.2384619"},{"key":"e_1_2_2_20_1","unstructured":"Florian Hahn. 2015. Rust2Viper: Building a static verifier for Rust. Master\u2019s thesis. ETH Zurich.  Florian Hahn. 2015. Rust2Viper: Building a static verifier for Rust. Master\u2019s thesis. ETH Zurich."},{"key":"e_1_2_2_21_1","volume-title":"Capabilities for Uniqueness and Borrowing. In European Conference on ObjectOriented Programming (ECOOP) (Lecture Notes in Computer Science) , Theo D\u2019Hondt (Ed.)","volume":"6183","author":"Haller Philipp","year":"2010"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_2_2_23_1","volume-title":"Ironclad Apps: End-to-End Security via Automated Full-System Verification. In Operating Systems Design and Implementation (OSDI)","author":"Hawblitzel Chris","year":"2014"},{"key":"e_1_2_2_24_1","volume-title":"Summers","author":"Heule Stefan","year":"2013"},{"key":"e_1_2_2_25_1","volume-title":"IFIP Congress. 321\u2013332","author":"Jones Cliff B.","year":"1983"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2676980"},{"key":"e_1_2_2_28_1","volume-title":"K-Rust: An Executable Formal Semantics for Rust. CoRR abs\/1804.07608","author":"Kan Shuanglong","year":"2018"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-010-0152-5"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_2_2_31_1","unstructured":"Gary T. Leavens Erik Poll Curtis Clifton Yoonsik Cheon Clyde Ruby David Cok Peter M\u00fcller Joseph Kiniry Patrice Chalin Daniel M. Zimmerman and Werner Dietl. 2011. JML Reference Manual. http:\/\/www.jmlspecs.org\/ .  Gary T. Leavens Erik Poll Curtis Clifton Yoonsik Cheon Clyde Ruby David Cok Peter M\u00fcller Joseph Kiniry Patrice Chalin Daniel M. Zimmerman and Werner Dietl. 2011. JML Reference Manual. http:\/\/www.jmlspecs.org\/ ."},{"key":"e_1_2_2_32_1","volume-title":"Dafny: An Automatic Program Verifier for Functional Correctness. In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR) (Lecture Notes in Computer Science) , Edmund M","author":"Leino K. Rustan M.","year":"2010"},{"key":"e_1_2_2_33_1","volume-title":"Object Invariants in Dynamic Contexts. In European Conference on Object-Oriented Programming (ECOOP) (Lecture Notes in Computer Science) , M. Odersky (Ed.)","volume":"3086","author":"K. Rustan"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/570886.570888"},{"key":"e_1_2_2_35_1","volume-title":"Industrial Informatics (INDIN)","author":"Lindner Marcus"},{"key":"e_1_2_2_36_1","doi-asserted-by":"crossref","unstructured":"Maroua Maalej Tucker Taft and Yannick Moy. 2018. Safe Dynamic Memory Management in Ada and SPARK. (2018).  Maroua Maalej Tucker Taft and Yannick Moy. 2018. Safe Dynamic Memory Management in Ada and SPARK. (2018).","DOI":"10.1007\/978-3-319-92432-8_3"},{"key":"e_1_2_2_37_1","unstructured":"Nicholas D. Matsakis. 2018a. MIR-based borrow check (NLL) status update. http:\/\/smallcultfollowing.com\/babysteps\/blog\/ 2018\/06\/15\/mir-based-borrow-check-nll-status-update Accessed April 4 2019.  Nicholas D. Matsakis. 2018a. MIR-based borrow check (NLL) status update. http:\/\/smallcultfollowing.com\/babysteps\/blog\/ 2018\/06\/15\/mir-based-borrow-check-nll-status-update Accessed April 4 2019."},{"key":"e_1_2_2_38_1","unstructured":"Nicholas D. Matsakis. 2018b. MIR-based borrowck is almost here. http:\/\/smallcultfollowing.com\/babysteps\/blog\/2018\/10\/ 31\/mir-based-borrowck-is-almost-here\/ Accessed April 4 2019.  Nicholas D. Matsakis. 2018b. MIR-based borrowck is almost here. http:\/\/smallcultfollowing.com\/babysteps\/blog\/2018\/10\/ 31\/mir-based-borrowck-is-almost-here\/ Accessed April 4 2019."},{"key":"e_1_2_2_39_1","volume-title":"Klock II","author":"Matsakis Nicholas D.","year":"2014"},{"key":"e_1_2_2_40_1","volume-title":"Advances in object-oriented software engineering","author":"Meyer Bertrand"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46406-9"},{"key":"e_1_2_2_42_1","volume-title":"Summers","author":"M\u00fcller Peter","year":"2016"},{"key":"e_1_2_2_43_1","volume-title":"Concurrency Theory (CONCUR) (Lecture Notes in Computer Science)","author":"O\u2019Hearn Peter W."},{"key":"e_1_2_2_44_1","volume-title":"Computer Science Logic (CSL) (Lecture Notes in Computer Science)","author":"O\u2019Hearn Peter W."},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360224"},{"key":"e_1_2_2_46_1","volume-title":"Bierman","author":"Parkinson Matthew J.","year":"2005"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(3:1)2012"},{"key":"e_1_2_2_48_1","volume-title":"Patina: A Formalization of the Rust Programming Language. Technical Report UW-CSE-15-03-02","author":"Reed Eric W.","year":"2015"},{"key":"e_1_2_2_49_1","volume-title":"Separation Logic: A Logic for Shared Mutable Data Structures. In Logic in Computer Science (LICS)","author":"Reynolds John C.","year":"2002"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1379022.1375602"},{"key":"e_1_2_2_51_1","volume-title":"https:\/\/rosettacode.org\/wiki\/Category:Rust Accessed","author":"Rosetta Code Rosetta Code","year":"2018"},{"key":"e_1_2_2_52_1","volume-title":"Non-Lexical Lifetimes RFC. https:\/\/github.com\/rust-lang\/rfcs\/blob\/master\/text\/2094-nll.md Accessed","author":"Rust","year":"2018"},{"key":"e_1_2_2_53_1","volume-title":"The Rust community\u2019s crate registry. https:\/\/crates.io Downloaded on","author":"Rust","year":"2018"},{"key":"e_1_2_2_54_1","volume-title":"Rust: The Reference \u2014 Place Expressions and Value Expressions. https:\/\/doc.rust-lang.org\/ reference\/expressions.html#place-expressions-and-value-expressions Accessed","author":"Rust","year":"2018"},{"key":"e_1_2_2_55_1","volume-title":"Learn Rust by writing Entirely Too Many Linked Lists. https:\/\/rust-unofficial.github.io\/too-manylists\/first-final.html Accessed","author":"Rust","year":"2019"},{"key":"e_1_2_2_56_1","volume-title":"The Polonius Reference Implementation for the Rust Borrow-Checker. https:\/\/github.com\/rustlang\/polonius Accessed","author":"Rust","year":"2019"},{"key":"e_1_2_2_57_1","volume-title":"The Rustonomicon: Working with Unsafe. https:\/\/doc.rust-lang.org\/nomicon\/working-withunsafe.html Accessed","author":"Rust","year":"2019"},{"key":"e_1_2_2_58_1","volume-title":"Tracking issue for generalized two-phase borrows. https:\/\/github.com\/rust-lang\/rust\/issues\/49434 Accessed","author":"Rust","year":"2019"},{"key":"e_1_2_2_59_1","volume-title":"European Conference on Object-Oriented Programming (ECOOP) (LIPIcs) , J. T. Boyland (Ed.)","volume":"37","author":"Schwerhoff Malte"},{"key":"e_1_2_2_60_1","volume-title":"Implicit Dynamic Frames: Combining Dynamic Frames and Separation Logic. In European Conference on Object-Oriented Programming (ECOOP) (Lecture Notes in Computer Science), Sophia Drossopoulou (Ed.)","volume":"5653","author":"Smans Jan","year":"2009"},{"key":"e_1_2_2_61_1","volume-title":"Formal Techniques for Distributed Systems (FMOODS\/FORTE) (Lecture Notes in Computer Science)","author":"Smans Jan"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/2543920"},{"key":"e_1_2_2_63_1","volume-title":"European Conference on Object-Oriented Programming (ECOOP) (Lecture Notes in Computer Science), Giuseppe Castagna (Ed.)","volume":"7920","author":"Alexander"},{"key":"e_1_2_2_64_1","volume-title":"Crust: A Bounded Verifier for Rust (N). In Automated Software Engineering (ASE) , Myra B","author":"Toman John","year":"2015"},{"key":"e_1_2_2_65_1","volume-title":"Simple Verification of Rust Programs via Functional Purification. Master\u2019s thesis","author":"Ullrich Sebastian"},{"key":"e_1_2_2_66_1","volume-title":"KRust: A Formal Executable Semantics of Rust. CoRR abs\/1804.10806","author":"Wang Feng","year":"2018"},{"key":"e_1_2_2_67_1","volume-title":"Rust Distilled: An Expressive Tower of Languages. arXiv preprint arXiv:1806.02693","author":"Weiss Aaron","year":"2018"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360573","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360573","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:22:59Z","timestamp":1750188179000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360573"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,10]]},"references-count":67,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2019,10,10]]}},"alternative-id":["10.1145\/3360573"],"URL":"https:\/\/doi.org\/10.1145\/3360573","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,10,10]]},"assertion":[{"value":"2019-10-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}