{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:35:28Z","timestamp":1781238928962,"version":"3.54.1"},"reference-count":55,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["683289"],"award-info":[{"award-number":["683289"]}],"id":[{"id":"10.13039\/501100000781","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,6,20]]},"abstract":"<jats:p>\n            Rust is a modern systems programming language whose ownership-based type system statically guarantees memory safety, making it particularly well-suited to the domain of safety-critical systems. In recent years, a wellspring of automated deductive verification tools have emerged for establishing functional correctness of Rust code. However, none of the previous tools produce\n            <jats:italic toggle=\"yes\">foundational<\/jats:italic>\n            proofs (machine-checkable in a generalpurpose proof assistant), and all of them are restricted to the\n            <jats:italic toggle=\"yes\">safe<\/jats:italic>\n            fragment of Rust. This is a problem because the vast majority of Rust programs make use of\n            <jats:italic toggle=\"yes\">unsafe<\/jats:italic>\n            code at critical points, such as in the implementation of widely-used APIs. We propose\n            <jats:italic toggle=\"yes\">RefinedRust<\/jats:italic>\n            , a refinement type system\u2014proven sound in the Coq proof assistant\u2014with the goal of establishing\n            <jats:italic toggle=\"yes\">foundational<\/jats:italic>\n            semi-automated functional correctness verification of both safe and unsafe Rust code. We have developed a prototype verification tool implementing RefinedRust. Our tool translates Rust code (with user annotations) into a model of Rust embedded in Coq, and then checks its adherence to the RefinedRust type system using separation logic automation in Coq. All proofs generated by RefinedRust are checked by the Coq proof assistant, so the automation and type system do not have to be trusted. We evaluate the effectiveness of RefinedRust by verifying a variant of Rust\u2019s\n            <jats:styled-content style=\"color:#008000\">\n              <jats:monospace>Vec<\/jats:monospace>\n            <\/jats:styled-content>\n            implementation that involves intricate reasoning about unsafe pointer-manipulating code.\n          <\/jats:p>","DOI":"10.1145\/3656422","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"1115-1139","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":31,"title":["RefinedRust: A Type System for High-Assurance Verification of Rust Programs"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2917-375X","authenticated-orcid":false,"given":"Lennard","family":"G\u00e4her","sequence":"first","affiliation":[{"name":"MPI-SWS, Saarland Informatics Campus, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4591-743X","authenticated-orcid":false,"given":"Michael","family":"Sammler","sequence":"additional","affiliation":[{"name":"MPI-SWS, Saarland Informatics Campus, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7669-6348","authenticated-orcid":false,"given":"Ralf","family":"Jung","sequence":"additional","affiliation":[{"name":"ETH Zurich, Z\u00fcrich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1185-5237","authenticated-orcid":false,"given":"Robbert","family":"Krebbers","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen, Nijmegen, Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3884-6867","authenticated-orcid":false,"given":"Derek","family":"Dreyer","sequence":"additional","affiliation":[{"name":"MPI-SWS, Saarland Informatics Campus, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_1_2_2","unstructured":"Andrew W. Appel. 2014. Program Logics for Certified Compilers. https:\/\/www.cambridge.org\/de\/academic\/subjects\/computer-science\/programming-languages-and-applied-logic\/program-logics-certified-compilers"},{"key":"e_1_3_1_3_2","unstructured":"Matt Asay. 2020. Why AWS loves Rust and how we\u2019d like to help. https:\/\/aws.amazon.com\/de\/blogs\/opensource\/why-aws-loves-rust-and-how-wed-like-to-help\/. Last accessed 07 October 2021."},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/3360573"},{"key":"e_1_3_1_5_2","unstructured":"The Rustonomicon authors. 2023. The nullable pointer optimization. https:\/\/doc.rust-lang.org\/nomicon\/ffi.html#the-nullable-pointer-optimization Last accessed 16 Nov 2023."},{"key":"e_1_3_1_6_2","unstructured":"The Rustonomicon authors. 2023. Vector implementation. https:\/\/doc.rust-lang.org\/nomicon\/vec\/vec-final.html Last accessed 16 Nov 2023."},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","unstructured":"David G. Clarke and Sophia Drossopoulou. 2002. Ownership encapsulation and the disjointness of type and effect. In OOPSLA. 292\u2013310. https:\/\/doi.org\/10.1145\/582419.582447 10.1145\/582419.582447","DOI":"10.1145\/582419.582447"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","unstructured":"David G. Clarke John M. Potter and James Noble. 1998. Ownership types for flexible alias protection. In OOPSLA. https:\/\/doi.org\/10.1145\/286936.286947 10.1145\/286936.286947","DOI":"10.1145\/286936.286947"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","unstructured":"Ernie Cohen Markus Dahlweid Mark A. Hillebrand Dirk Leinenbach Michal Moskal Thomas Santen Wolfram Schulte and Stephan Tobies. 2009. VCC: A Practical System for Verifying Concurrent C. In TPHOLs (LNCS Vol.5674). 23\u201342. https:\/\/doi.org\/10.1007\/978-3-642-03359-9_2 10.1007\/978-3-642-03359-9_2","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17244-1_6"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","unstructured":"Ronghui Gu Zhong Shao Jieung Kim Xiongnan (Newman) Wu J\u00e9r\u00e9mie Koenig Vilhelm Sj\u00f6berg Hao Chen David Costanzo and Tahina Ramananandro. 2018. Certified concurrent abstraction layers. In PLDI. 646\u2013661. https:\/\/doi.org\/10.1145\/3192366.3192381 10.1145\/3192366.3192381","DOI":"10.1145\/3192366.3192381"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","unstructured":"Lennard G\u00e4her Michael Sammler Ralf Jung Robbert Krebbers and Derek Dreyer. 2023. RefinedRust: Technical Documentation and Coq Development. https:\/\/doi.org\/10.5281\/zenodo.10912439 10.5281\/zenodo.10912439 Project website: https:\/\/plv.mpisws.org\/refinedrust\/.","DOI":"10.5281\/zenodo.10912439"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3547647"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","unstructured":"Bart Jacobs Jan Smans Pieter Philippaerts Fr\u00e9d\u00e9ric Vogels Willem Penninckx and Frank Piessens. 2011. VeriFast: A Powerful Sound Predictable Fast Verifier for C and Java. In NASA Formal Methods (LNCS Vol. 6617). 41\u201355 https:\/\/doi.org\/10.1007\/978-3-642-20398-5_4 10.1007\/978-3-642-20398-5_4","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_3_1_15_2","unstructured":"Trevor Jim J. Gregory Morrisett Dan Grossman Michael W. Hicks James Cheney and Yanling Wang. 2002. Cyclone: A safe dialect of C. In USENIX ATC. 275\u2013288. http:\/\/www.usenix.org\/publications\/library\/proceedings\/usenix02\/jim.html"},{"key":"e_1_3_1_16_2","volume-title":"Understanding and evolving the Rust programming language","author":"Jung Ralf","year":"2020","unstructured":"Ralf Jung. 2020. Understanding and evolving the Rust programming language. Ph. D. Dissertation. Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany. https:\/\/publikationen.sulb.uni-saarland.de\/handle\/20.500.11880\/29647"},{"key":"e_1_3_1_17_2","unstructured":"Ralf Jung. 2023. MiniRust. https:\/\/github.com\/RalfJung\/minirust Last accessed 16 Nov 2023."},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371109"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","unstructured":"Ralf Jung Robbert Krebbers Lars Birkedal and Derek Dreyer. 2016. Higher-order ghost state. In ICFP. 256\u2013269. https:\/\/doi.org\/10.1145\/2951913.2951943 10.1145\/2951913.2951943","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","unstructured":"Ralf Jung David Swasey Filip Sieczkowski Kasper Svendsen Aaron Turon Lars Birkedal and Derek Dreyer. 2015. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. In POPL. 637\u2013650. https:\/\/doi.org\/10.1145\/2676726.2676980 10.1145\/2676726.2676980","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_1_23_2","unstructured":"Shuanglong Kan David San\u00e1n Shang-Wei Lin and Yang Liu. 2020. An Executable Operational Semantics for Rust with the Formalization of Ownership and Borrowing. CoRR abs\/1804.07608 (2020). http:\/\/arxiv.org\/abs\/1804.07608"},{"key":"e_1_3_1_24_2","unstructured":"The Kani Developers. 2022. The Kani Rust Verifier. https:\/\/github.com\/model-checking\/kani Last accessed 01 October 2022."},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","unstructured":"Gerwin Klein Kevin Elphinstone Gernot Heiser June Andronick David Cock Philip Derrin Dhammika Elkaduwe Kai Engelhardt Rafal Kolanski Michael Norrish Thomas Sewell Harvey Tuch and Simon Winwood. 2009. seL4: Formal verification of an OS kernel. In SOSP. 207\u2013220. https:\/\/doi.org\/10.1145\/1629575.1629596 10.1145\/1629575.1629596","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","unstructured":"Robbert Krebbers Ralf Jung Ales Bizjak Jacques-Henri Jourdan Derek Dreyer and Lars Birkedal. 2017. The Essence of Higher-Order Concurrent Separation Logic. In ESOP (LNCS Vol. 10201). 696\u2013723. https:\/\/doi.org\/10.1007\/978-3-662-54434-1_26 10.1007\/978-3-662-54434-1_26","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","unstructured":"Robbert Krebbers Amin Timany and Lars Birkedal. 2017. Interactive proofs in higher-order concurrent separation logic. In POPL. 205\u2013217. https:\/\/doi.org\/10.1145\/3009837.3009855 10.1145\/3009837.3009855","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3586037"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591283"},{"key":"e_1_3_1_30_2","unstructured":"Xavier Leroy Andrew Appel Sandrine Blazy and Gordon Stewart. 2012. The CompCert memory model version 2. Technical Report RR-7987. Inria. https:\/\/hal.inria.fr\/hal-00703441"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_38"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","unstructured":"Yusuke Matsushita Xavier Denis Jacques-Henri Jourdan and Derek Dreyer. 2022. RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe code. In PLDI. ACM. https:\/\/doi.org\/10.1145\/3519939.3523704 10.1145\/3519939.3523704","DOI":"10.1145\/3519939.3523704"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_18"},{"key":"e_1_3_1_34_2","unstructured":"The Miri Developers. 2015. Miri: An interpreter for Rust\u2019s mid-level intermediate representation. https:\/\/github.com\/rust-lang\/miri Last accessed 24 October 2022."},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","unstructured":"Edgar Pek Xiaokang Qiu and P. Madhusudan. 2014. Natural proofs for data structure manipulation in C using separation logic. In PLDI. ACM 440\u2013451. https:\/\/doi.org\/10.1145\/2594291.2594325 10.1145\/2594291.2594325","DOI":"10.1145\/2594291.2594325"},{"key":"e_1_3_1_37_2","unstructured":"Polonius. 2018. Rust Polonius. https:\/\/github.com\/rust-lang\/polonius. Last accessed 03 October 2021."},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571194"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","unstructured":"Patrick Maxim Rondon Ming Kawaguchi and Ranjit Jhala. 2008. Liquid types. In PLDI. 159\u2013169. https:\/\/doi.org\/10.1145\/1375581.1375602 10.1145\/1375581.1375602","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2010.03.012"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.22028\/D291-41316"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","unstructured":"Michael Sammler Rodolphe Lepigre Robbert Krebbers Kayvan Memarian Derek Dreyer and Deepak Garg. 2021. RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types. In PLDI. 158\u2013174. https:\/\/doi.org\/10.1145\/3453483.3454036 10.1145\/3453483.3454036","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","unstructured":"Jos\u00e9 Fragoso Santos Petar Maksimovic Sacha-\u00c9lie Ayoun and Philippa Gardner. 2020. Gillian part i: a multi-language platform for symbolic execution. In PLDI. ACM 927\u2013942. https:\/\/doi.org\/10.1145\/3385412.3386014 10.1145\/3385412.3386014","DOI":"10.1145\/3385412.3386014"},{"key":"e_1_3_1_44_2","volume-title":"CreuSAT, Using Rust and Creusot to create the world\u2019s fastest deductively verified SAT solver","author":"Skot\u00e5m Sarek H\u00f8verstad","year":"2022","unstructured":"Sarek H\u00f8verstad Skot\u00e5m. 2022. CreuSAT, Using Rust and Creusot to create the world\u2019s fastest deductively verified SAT solver. Master\u2019s thesis. University of Oslo. https:\/\/www.duo.uio.no\/handle\/10852\/96757"},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/3547631"},{"key":"e_1_3_1_46_2","unstructured":"Jeff Vander Stoep and Stephen Hines. 2021. Rust in the Android platform. https:\/\/security.googleblog.com\/2021\/04\/rust-in-android-platform.html. Last accessed 07 October 2021."},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","unstructured":"Alexander J. Summers and Peter M\u00fcller. 2018. Automating Deductive Verification for Weak-Memory Programs. 10805 (2018) 190\u2013209. https:\/\/doi.org\/10.1007\/978-3-319-89960-2_11 10.1007\/978-3-319-89960-2_11","DOI":"10.1007\/978-3-319-89960-2_11"},{"key":"e_1_3_1_48_2","unstructured":"The Rust Team. 2020. The Rust programming language. https:\/\/rust-lang.org."},{"key":"e_1_3_1_49_2","doi-asserted-by":"crossref","unstructured":"Amin Timany Robbert Krebbers Derek Dreyer and Lars Birkedal. 2024. A Logical Approach to Type Soundness. https:\/\/iris-project.org\/pdfs\/2024-submitted-logical-type-soundness.pdf Manuscript.","DOI":"10.1145\/3676954"},{"key":"e_1_3_1_50_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.2613"},{"key":"e_1_3_1_51_2","unstructured":"Linus Torvalds. 2022. Merge Commit for initial Rust support in the Linux kernel. https:\/\/git.kernel.org\/pub\/scm\/linux\/kernel\/git\/torvalds\/linux.git\/commit\/?id=8aebac82933ff1a7c8eede18cab11e1115e2062b Last accessed 24 Oct 2022."},{"key":"e_1_3_1_52_2","volume-title":"Advanced Topics in Types and Programming Languages","author":"Walker David","year":"2005","unstructured":"David Walker. 2005. Substructural Type Systems. In Advanced Topics in Types and Programming Languages, Benjamin C. Pierce (Ed.). MIT Press."},{"key":"e_1_3_1_53_2","doi-asserted-by":"publisher","unstructured":"Feng Wang Fu Song Min Zhang Xiaoran Zhu and Jun Zhang. 2018. KRust: A Formal Executable Semantics of Rust. In TASE. IEEE Computer Society 44\u201351. https:\/\/doi.org\/10.1109\/TASE.2018.00014 10.1109\/TASE.2018.00014","DOI":"10.1109\/TASE.2018.00014"},{"key":"e_1_3_1_54_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-022-09654-Y"},{"key":"e_1_3_1_55_2","doi-asserted-by":"publisher","DOI":"10.1145\/3485522"},{"key":"e_1_3_1_56_2","unstructured":"Sacha \u00c9lie Ayoun Xavier Denis Petar Maksimovi\u0107 and Philippa Gardner. 2024. A hybrid approach to semi-automated Rust verification. arXiv:2403.15122 [cs.PL] https:\/\/arxiv.org\/abs\/2403.15122"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656422","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656422","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:43:32Z","timestamp":1751661812000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656422"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":55,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656422"],"URL":"https:\/\/doi.org\/10.1145\/3656422","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}