{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T14:14:09Z","timestamp":1784211249214,"version":"3.55.0"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T00:00:00Z","timestamp":1767830400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"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>\n                    The Rust programming language has two faces: on the one hand, it is a high-level language with a strong type system ensuring memory and thread safety. On the other hand, Rust crucially relies on\n                    <jats:italic toggle=\"yes\">unsafe code<\/jats:italic>\n                    for cases where the compiler is unable to statically ensure basic safety properties. The challenges of writing unsafe Rust are similar to those of writing C or C++: a single mistake in the program can lead to\n                    <jats:italic toggle=\"yes\">Undefined Behavior<\/jats:italic>\n                    , 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.\n                  <\/jats:p>\n                  <jats:p>\n                    Ensuring the absence of Undefined Behavior bugs is therefore a high priority for unsafe Rust authors. In this paper we present\n                    <jats:italic toggle=\"yes\">Miri<\/jats:italic>\n                    , the first tool that can find\n                    <jats:italic toggle=\"yes\">all<\/jats:italic>\n                    de-facto Undefined Behavior in deterministic Rust programs. Some 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. In an evaluation on more than 100\u00a0000 Rust libraries, Miri was able to successfully execute more than 70% of the tests across their combined test suites. Miri 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.\n                  <\/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":4,"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"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3160-7679","authenticated-orcid":false,"given":"Benjamin","family":"Kimock","sequence":"additional","affiliation":[{"name":"Lansweeper NV, Silver Spring, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0890-9473","authenticated-orcid":false,"given":"Christian","family":"Poveda","sequence":"additional","affiliation":[{"name":"Unaffiliated, Bogot\u00e1, Colombia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"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"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-1731-1081","authenticated-orcid":false,"given":"Oli","family":"Scherer","sequence":"additional","affiliation":[{"name":"Unaffiliated, Karlsruhe, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-0779-8651","authenticated-orcid":false,"given":"Qian","family":"Wang","sequence":"additional","affiliation":[{"name":"Unaffiliated, London, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/3360573"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/3729289"},{"key":"e_1_3_2_4_2","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_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/2618128.2618134"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/3477132.3483540"},{"key":"e_1_3_2_7_2","unstructured":"David Peter. Last accessed July 10th 2025. Hyperfine. https:\/\/github.com\/sharkdp\/hyperfine."},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17244-1_6"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/1839676.1839699"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2212.12976"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656422"},{"key":"e_1_3_2_12_2","unstructured":"Jens Gustedt Peter Sewell Kayvan Memarian Victor B. F. Gomes and Martin Uecker. 2022. Programming languages -- A Provenance-aware memory object model for C. Technical Report. https:\/\/www.open-std.org\/jtc1\/sc22\/wg14\/www\/docs\/n3057.pdf"},{"key":"e_1_3_2_13_2","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_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3547647"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371109"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/3418295"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","unstructured":"Ralf Jung Benjamin Kimock Christian Poveda Eduardo S\u00e1nchez Mu\u00f1oz Oli Scherer and Qian Wang. 2026. Artifact for Miri: Practical Undefined Behavior Detection for Rust. doi:10.5281\/zenodo.17334726 (latest version available on paper website: https:\/\/plf.inf.ethz.ch\/research\/popl26-miri.html).","DOI":"10.5281\/zenodo.17334726"},{"key":"e_1_3_2_18_2","unstructured":"The Kani Developers. 2022. The Kani Rust Verifier. https:\/\/github.com\/model-checking\/kani Last accessed 01 July 2025."},{"key":"e_1_3_2_19_2","unstructured":"Paul Kehrer. 2019. Memory Unsafety in Apple's Operating Systems. https:\/\/langui.sh\/2019\/07\/23\/apple-memory-safety\/."},{"key":"e_1_3_2_20_2","unstructured":"Robbert Krebbers. 2015. The C standard formalized in Coq. Ph.D. Dissertation. Radboud University Nijmegen. https:\/\/robbertkrebbers.nl\/thesis.html"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/2676724.2693571"},{"key":"e_1_3_2_22_2","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\u2013632. doi:10.1145\/3062341.3062352","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3586037"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591283"},{"key":"e_1_3_2_25_2","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. doi:10.1145\/1111037.1111042","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_3_2_26_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_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009857"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","unstructured":"Roy Margalit and Ori Lahav. 2021. Verifying observational robustness against a c11-style memory model. In POPL. 4:1\u20134:33. doi:10.1145\/3434285","DOI":"10.1145\/3434285"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE55347.2025.00167"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290380"},{"key":"e_1_3_2_31_2","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. doi:10.1145\/2908080.2908081","DOI":"10.1145\/2908080.2908081"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0920-5489(01)00059-9"},{"key":"e_1_3_2_33_2","unstructured":"The Chromium Projects. Last accessed July 9th 2025. Memory safety. https:\/\/www.chromium.org\/Home\/chromium-security\/memory-safety\/."},{"key":"e_1_3_2_34_2","unstructured":"Rain. Last accessed July 10th 2025. cargo-nextest. https:\/\/github.com\/nextest-rs\/nextest."},{"key":"e_1_3_2_35_2","unstructured":"Runtime Verification. Last accessed July 10th 2025. RV-Match. https:\/\/runtimeverification.com\/match."},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993520"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/3689733"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454084"},{"key":"e_1_3_2_39_2","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_3_2_40_2","unstructured":"The Rust Team. 2020. The Rust programming language. https:\/\/rust-lang.org."},{"key":"e_1_3_2_41_2","unstructured":"TrustInSoft. Last accessed July 10th 2025. TrustInSoft Analyzer. https:\/\/www.trust-in-soft.com\/trustinsoft-analyzer."},{"key":"e_1_3_2_42_2","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_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/3735592"},{"key":"e_1_3_2_44_2","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,7,16]],"date-time":"2026-07-16T13:39:08Z","timestamp":1784209148000},"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"}}]}}