{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,26]],"date-time":"2026-02-26T03:37:43Z","timestamp":1772077063829,"version":"3.50.1"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,1,8]]},"abstract":"<jats:p>The Rust programming language has two faces:  \non the one hand, it is a high-level language with a strong type system ensuring memory and thread safety.  \nOn the other hand, Rust crucially relies on unsafe code for cases where the compiler is unable to statically ensure basic safety properties.  \nThe challenges of writing unsafe Rust are similar to those of writing C or C++: a single mistake in the program can lead to Undefined Behavior, which means the program is no longer described by the language's Abstract Machine and can go wrong in arbitrary ways, often causing security issues.<\/jats:p>\n                  <jats:p>Ensuring the absence of Undefined Behavior bugs is therefore a high priority for unsafe Rust authors.  \nIn this paper we present Miri, the first tool that can find all de-facto Undefined Behavior in deterministic Rust programs.  \nSome of the key non-trivial features of Miri include tracking of pointer provenance, validation of Rust type invariants, data-race detection, exploration of weak memory behaviors, and implementing enough basic OS APIs (such as file system access and concurrency primitives) to be able to run unchanged real-world Rust code.  \nIn an evaluation on more than 100 000 Rust libraries, Miri was able to successfully execute more than 70% of the tests across their combined test suites.  \nMiri has found dozens of real-world bugs and has been integrated into the continuous integration of the Rust standard library and many prominent Rust libraries, preventing many more bugs from ever entering these codebases.<\/jats:p>","DOI":"10.1145\/3776690","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"1383-1411","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Miri: Practical Undefined Behavior Detection for Rust"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7669-6348","authenticated-orcid":false,"given":"Ralf","family":"Jung","sequence":"first","affiliation":[{"name":"ETH Zurich, Z\u00fcrich, Switzerland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3160-7679","authenticated-orcid":false,"given":"Benjamin","family":"Kimock","sequence":"additional","affiliation":[{"name":"Lansweeper NV, Silver Spring, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0890-9473","authenticated-orcid":false,"given":"Christian","family":"Poveda","sequence":"additional","affiliation":[{"name":"Unaffiliated, Bogot\u00e1, Colombia"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6627-4459","authenticated-orcid":false,"given":"Eduardo S\u00e1nchez","family":"Mu\u00f1oz","sequence":"additional","affiliation":[{"name":"Unaffiliated, Oviedo, Spain"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-1731-1081","authenticated-orcid":false,"given":"Oli","family":"Scherer","sequence":"additional","affiliation":[{"name":"Unaffiliated, Karlsruhe, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-0779-8651","authenticated-orcid":false,"given":"Qian","family":"Wang","sequence":"additional","affiliation":[{"name":"Unaffiliated, London, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360573"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3729289"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","unstructured":"Mark Batty Scott Owens Susmit Sarkar Peter Sewell and Tjark Weber. 2011. Mathematizing C++ concurrency. In POPL. 55\u201366. https:\/\/doi.org\/10.1145\/1926385.1926394 10.1145\/1926385.1926394","DOI":"10.1145\/1926385.1926394"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2618128.2618134"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477132.3483540"},{"key":"e_1_2_1_6_1","volume-title":"Last accessed July 10th","author":"Peter David","year":"2025","unstructured":"David Peter. Last accessed July 10th, 2025. Hyperfine. https:\/\/github.com\/sharkdp\/hyperfine"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17244-1_6"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1839676.1839699"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2212.12976"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656422"},{"key":"e_1_2_1_11_1","unstructured":"Jens Gustedt Peter Sewell Kayvan Memarian Victor B. F. Gomes and Martin Uecker. 2022. Programming languages \u2013 A Provenance-aware memory object model for C. https:\/\/www.open-std.org\/jtc1\/sc22\/wg14\/www\/docs\/n3057.pdf"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","unstructured":"Chris Hathhorn Chucky Ellison and Grigore Rosu. 2015. Defining the undefinedness of C. In PLDI. 336\u2013345. https:\/\/doi.org\/10.1145\/2737924.2737979 10.1145\/2737924.2737979","DOI":"10.1145\/2737924.2737979"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547647"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371109"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3418295"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.17334726"},{"key":"e_1_2_1_17_1","volume-title":"The Kani Rust Verifier. https:\/\/github.com\/model-checking\/kani Last accessed","author":"Developers The Kani","year":"2025","unstructured":"The Kani Developers. 2022. The Kani Rust Verifier. https:\/\/github.com\/model-checking\/kani Last accessed 01 July 2025"},{"key":"e_1_2_1_18_1","unstructured":"Paul Kehrer. 2019. Memory Unsafety in Apple\u2019s Operating Systems. https:\/\/langui.sh\/2019\/07\/23\/apple-memory-safety\/"},{"key":"e_1_2_1_19_1","volume-title":"The C standard formalized in Coq. Ph. D. Dissertation","author":"Krebbers Robbert","unstructured":"Robbert Krebbers. 2015. The C standard formalized in Coq. Ph. D. Dissertation. Radboud University Nijmegen. https:\/\/robbertkrebbers.nl\/thesis.html"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","unstructured":"Robbert Krebbers and Freek Wiedijk. 2015. A Typed C11 Semantics for Interactive Theorem Proving. In CPP. ACM 15\u201327. https:\/\/doi.org\/10.1145\/2676724.2693571 10.1145\/2676724.2693571","DOI":"10.1145\/2676724.2693571"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","unstructured":"Ori Lahav Viktor Vafeiadis Jeehoon Kang Chung-Kil Hur and Derek Dreyer. 2017. Repairing sequential consistency in C\/C++11. In PLDI. 618\u2013\u2013632. https:\/\/doi.org\/10.1145\/3062341.3062352 10.1145\/3062341.3062352","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586037"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591283"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","unstructured":"Xavier Leroy. 2006. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In POPL. 42\u201354. https:\/\/doi.org\/10.1145\/1111037.1111042 10.1145\/1111037.1111042","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_2_1_25_1","unstructured":"Xavier Leroy Andrew Appel Sandrine Blazy and Gordon Stewart. 2012. The CompCert memory model version 2. Inria. https:\/\/hal.inria.fr\/hal-00703441"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009857"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434285"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE55347.2025.00167"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290380"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","unstructured":"Kayvan Memarian Justus Matthiesen James Lingard Kyndylan Nienhuis David Chisnall Robert N. M. Watson and Peter Sewell. 2016. Into the depths of C: Elaborating the de facto standards. In PLDI. 1\u201315. https:\/\/doi.org\/10.1145\/2908080.2908081 10.1145\/2908080.2908081","DOI":"10.1145\/2908080.2908081"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0920-5489(01)00059-9"},{"key":"e_1_2_1_32_1","volume-title":"Last accessed July 9th","author":"Projects The Chromium","year":"2025","unstructured":"The Chromium Projects. Last accessed July 9th, 2025. Memory safety. https:\/\/www.chromium.org\/Home\/chromium-security\/memory-safety\/"},{"key":"e_1_2_1_33_1","volume-title":"Last accessed July 10th","year":"2025","unstructured":"Rain. Last accessed July 10th, 2025. cargo-nextest. https:\/\/github.com\/nextest-rs\/nextest"},{"key":"e_1_2_1_34_1","volume-title":"Last accessed July 10th","author":"Verification Runtime","year":"2025","unstructured":"Runtime Verification. Last accessed July 10th, 2025. RV-Match. https:\/\/runtimeverification.com\/match"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","unstructured":"Susmit Sarkar Peter Sewell Jade Alglave Luc Maranget and Derek Williams. 2011. Understanding POWER multiprocessors. In PLDI. ACM 175\u2013186. https:\/\/doi.org\/10.1145\/1993498.1993520 10.1145\/1993498.1993520","DOI":"10.1145\/1993498.1993520"},{"key":"e_1_2_1_36_1","volume-title":"Proc. ACM Program. Lang., 8, OOPSLA2","author":"Takashima Yoshiki","year":"2024","unstructured":"Yoshiki Takashima, Chanhee Cho, Ruben Martins, Limin Jia, and Corina S. Pasareanu. 2024. Crabtree: Rust API Test Synthesis Guided by Coverage and Type. Proc. ACM Program. Lang., 8, OOPSLA2 (2024), 618\u2013647."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454084"},{"key":"e_1_2_1_38_1","unstructured":"MSRC Team. 2019. A proactive approach to more secure code. https:\/\/msrc.microsoft.com\/blog\/2019\/07\/a-proactive-approach-to-more-secure-code\/"},{"key":"e_1_2_1_39_1","unstructured":"The Rust Team. 2020. The Rust programming language. https:\/\/rust-lang.org"},{"key":"e_1_2_1_40_1","volume-title":"Last accessed July 10th","year":"2025","unstructured":"TrustInSoft. Last accessed July 10th, 2025. TrustInSoft Analyzer. https:\/\/www.trust-in-soft.com\/trustinsoft-analyzer"},{"key":"e_1_2_1_41_1","volume-title":"Last changed","year":"2016","unstructured":"TrustInSoft. Last changed 2016. TIS Interpreter (in the Software Heritage Archive). https:\/\/archive.softwareheritage.org\/browse\/origin\/directory\/?origin_url=https:\/\/github.com\/TrustInSoft\/tis-interpreter"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3735592"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689780"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776690","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T19:00:09Z","timestamp":1767898809000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776690"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":43,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776690"],"URL":"https:\/\/doi.org\/10.1145\/3776690","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}