{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,21]],"date-time":"2026-03-21T03:17:23Z","timestamp":1774063043477,"version":"3.50.1"},"reference-count":70,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2021,10,31]],"date-time":"2021-10-31T00:00:00Z","timestamp":1635638400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"JSPS KAKENHI","award":["JP15H05706, JP16K16004, JP20H05703, and JP21J20459"],"award-info":[{"award-number":["JP15H05706, JP16K16004, JP20H05703, and JP21J20459"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2021,12,31]]},"abstract":"<jats:p>Reduction to satisfiability of constrained Horn clauses (CHCs) is a widely studied approach to automated program verification. Current CHC-based methods, however, do not work very well for pointer-manipulating programs, especially those with dynamic memory allocation. This article presents a novel reduction of pointer-manipulating Rust programs into CHCs, which clears away pointers and memory states by leveraging Rust\u2019s guarantees on permission. We formalize our reduction for a simplified core of Rust and prove its soundness and completeness. We have implemented a prototype verifier for a subset of Rust and confirmed the effectiveness of our method.<\/jats:p>","DOI":"10.1145\/3462205","type":"journal-article","created":{"date-parts":[[2021,11,1]],"date-time":"2021-11-01T00:41:27Z","timestamp":1635727287000},"page":"1-54","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":50,"title":["RustHorn: CHC-based Verification for Rust Programs"],"prefix":"10.1145","volume":"43","author":[{"given":"Yusuke","family":"Matsushita","sequence":"first","affiliation":[{"name":"The University of Tokyo, Tokyo, Japan"}]},{"given":"Takeshi","family":"Tsukada","sequence":"additional","affiliation":[{"name":"Chiba University, Chiba, Japan"}]},{"given":"Naoki","family":"Kobayashi","sequence":"additional","affiliation":[{"name":"The University of Tokyo, Tokyo, Japan"}]}],"member":"320","published-online":{"date-parts":[[2021,10,31]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28717-6_7"},{"key":"e_1_3_2_4_2","doi-asserted-by":"crossref","unstructured":"Vytautas Astrauskas Peter M\u00fcller Federico Poli and Alexander J. Summers. 2018. Leveraging Rust types for modular specification and verification. DOI:DOI:https:\/\/doi.org\/10.3929\/ethz-b-000311092","DOI":"10.1145\/3360573"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01090-4_32"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/1953122.1953145"},{"key":"e_1_3_2_7_2","first-page":"24","volume-title":"Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday (Lecture Notes in Computer Science)","author":"Bj\u00f8rner Nikolaj","year":"2015","unstructured":"Nikolaj Bj\u00f8rner, Arie Gurfinkel, Kenneth L. McMillan, and Andrey Rybalchenko. 2015. Horn clause solvers for program verification. In Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday (Lecture Notes in Computer Science), Lev D. Beklemishev, Andreas Blass, Nachum Dershowitz, Bernd Finkbeiner, and Wolfram Schulte (Eds.), Vol. 9300. Springer, 24\u201351. DOI:DOI:https:\/\/doi.org\/10.1007\/978-3-319-23534-9_2"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/1047659.1040327"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/583854.582440"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.5555\/1760267.1760273"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_28"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158099"},{"key":"e_1_3_2_13_2","first-page":"365","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14\u201320, 2018, Proceedings, Part I (Lecture Notes in Computer Science)","volume":"10805","author":"Champion Adrien","year":"2018","unstructured":"Adrien Champion, Tomoya Chiba, Naoki Kobayashi, and Ryosuke Sato. 2018. ICE-based refinement type discovery for higher-order functional programs. In Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14\u201320, 2018, Proceedings, Part I (Lecture Notes in Computer Science), Dirk Beyer and Marieke Huisman (Eds.), Vol. 10805. Springer, 365\u2013384. DOI:DOI:https:\/\/doi.org\/10.1007\/978-3-319-89960-2_20"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02768-1_8"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/286942.286947"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"e_1_3_2_17_2","unstructured":"Coq Team. 2021. The Coq Proof Assistant. Retrieved from https:\/\/coq.inria.fr\/."},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"e_1_3_2_19_2","unstructured":"Dropbox. 2020. Rewriting the Heart of Our Sync Engine - Dropbox. Retrieved from https:\/\/dropbox.tech\/infrastructure\/rewriting-the-heart-of-our-sync-engine."},{"key":"e_1_3_2_20_2","volume-title":"Verification of Rust Generics, Typestates, and Traits","author":"Erdin Matthias","year":"2019","unstructured":"Matthias Erdin. 2019. Verification of Rust Generics, Typestates, and Traits. Master\u2019s thesis. ETH Z\u00fcrich."},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.5555\/3168451.3168476"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_14"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/1232420.1232424"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/2345156.2254112"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66706-5_8"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950330"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01090-4_15"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009893"},{"key":"e_1_3_2_32_2","first-page":"1","volume-title":"2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30\u2013November 2, 2018","author":"Hojjat Hossein","year":"2018","unstructured":"Hossein Hojjat and Philipp R\u00fcmmer. 2018. The eldarica Horn solver. In 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30\u2013November 2, 2018, Nikolaj Bj\u00f8rner and Arie Gurfinkel (Eds.). IEEE, 1\u20137. DOI:DOI:https:\/\/doi.org\/10.23919\/FMCAD.2018.8603013"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.2307\/2268661"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.5555\/647057.713871"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371113"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/2775051.2676980"},{"key":"e_1_3_2_39_2","first-page":"368","volume-title":"LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7\u201312, 2017 (EPiC Series in Computing)","author":"Kahsai Temesghen","year":"2017","unstructured":"Temesghen Kahsai, Rody Kersten, Philipp R\u00fcmmer, and Martin Sch\u00e4f. 2017. Quantified heap invariants for object-oriented programs. In LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7\u201312, 2017 (EPiC Series in Computing), Thomas Eiter and David Sands (Eds.), Vol. 46. EasyChair, 368\u2013384."},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_19"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2018.23082"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993525"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_2"},{"key":"e_1_3_2_44_2","first-page":"569","volume-title":"Information Processing, Proceedings of the 6th IFIP Congress 1974, Stockholm, Sweden, August 5\u201310, 1974","author":"Kowalski Robert A.","year":"1974","unstructured":"Robert A. Kowalski. 1974. Predicate logic as programming language. In Information Processing, Proceedings of the 6th IFIP Congress 1974, Stockholm, Sweden, August 5\u201310, 1974, Jack L. Rosenfeld (Ed.). North-Holland, 569\u2013574."},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_22"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01090-4"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1109\/INDIN.2018.8471992"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/2692956.2663188"},{"key":"e_1_3_2_50_2","first-page":"484","volume-title":"Programming Languages and Systems - 29th European Symposium on Programming, ESOP 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings (Lecture Notes in Computer Science)","volume":"12075","author":"Matsushita Yusuke","year":"2020","unstructured":"Yusuke Matsushita, Takeshi Tsukada, and Naoki Kobayashi. 2020. RustHorn: CHC-based verification for Rust programs. In Programming Languages and Systems - 29th European Symposium on Programming, ESOP 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings (Lecture Notes in Computer Science), Peter M\u00fcller (Ed.), Vol. 12075. Springer, 484\u2013514. DOI:DOI:https:\/\/doi.org\/10.1007\/978-3-030-44914-8_18"},{"key":"e_1_3_2_51_2","unstructured":"Microsoft. 2021. Boogie: An Intermediate Verification Language. Retrieved from https:\/\/www.microsoft.com\/en-us\/research\/project\/boogie-an-intermediate-verification-language\/."},{"key":"e_1_3_2_52_2","unstructured":"Mozilla. 2021. Rust language \u2014 Mozilla Research. Retrieved from https:\/\/research.mozilla.org\/rust\/."},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_3_2_54_2","unstructured":"npm. 2019. Rust Case Study: Community Makes Rust an Easy Choice for npm. Retrieved from https:\/\/www.rust-lang.org\/static\/pdfs\/Rust-npm-Whitepaper.pdf."},{"key":"e_1_3_2_55_2","unstructured":"Rust Community. 2021. The MIR (Mid-level IR). Retrieved from https:\/\/rustc-dev-guide.rust-lang.org\/mir\/index.html."},{"key":"e_1_3_2_56_2","unstructured":"Rust Community. 2021. Reference Cycles Can Leak Memory - The Rust Programming Language. Retrieved from https:\/\/doc.rust-lang.org\/book\/ch15-06-reference-cycles.html."},{"key":"e_1_3_2_57_2","unstructured":"Rust Community. 2021. RFC 2025: Nested Method Calls. Retrieved from https:\/\/rust-lang.github.io\/rfcs\/2025-nested-method-calls.html."},{"key":"e_1_3_2_58_2","unstructured":"Rust Community. 2021. RFC 2094: Non-lexical Lifetimes. Retrieved from https:\/\/rust-lang.github.io\/rfcs\/2094-nll.html."},{"key":"e_1_3_2_59_2","unstructured":"Rust Community. 2021. Rust Programming Language. Retrieved from https:\/\/www.rust-lang.org\/."},{"key":"e_1_3_2_60_2","unstructured":"Rust Community. 2021. std::cell::RefCell - Rust. Retrieved from https:\/\/doc.rust-lang.org\/std\/cell\/struct.RefCell.html."},{"key":"e_1_3_2_61_2","unstructured":"Rust Community. 2021. std::collections::HashMap - Rust. Retrieved from https:\/\/doc.rust-lang.org\/std\/collections\/struct.HashMap.html."},{"key":"e_1_3_2_62_2","unstructured":"Rust Community. 2021. std::rc::Rc - Rust. Retrieved from https:\/\/doc.rust-lang.org\/std\/rc\/struct.Rc.html."},{"key":"e_1_3_2_63_2","unstructured":"Rust Community. 2021. std::sync::Mutex - Rust. Retrieved from https:\/\/doc.rust-lang.org\/std\/sync\/struct.Mutex.html."},{"key":"e_1_3_2_64_2","unstructured":"Rust Community. 2021. std::thread::spawn - Rust. Retrieved from https:\/\/doc.rust-lang.org\/std\/thread\/fn.spawn.html."},{"key":"e_1_3_2_65_2","unstructured":"Rust Community. 2021. std::vec::Vec - Rust. Retrieved from https:\/\/doc.rust-lang.org\/std\/vec\/struct.Vec.html."},{"key":"e_1_3_2_66_2","unstructured":"Rust Community. 2021. Two-phase borrows. Retrieved from https:\/\/rust-lang.github.io\/rustc-guide\/borrow_check\/two_phase_borrows.html."},{"key":"e_1_3_2_67_2","doi-asserted-by":"publisher","DOI":"10.1145\/3294032.3294081"},{"key":"e_1_3_2_68_2","doi-asserted-by":"publisher","DOI":"10.5555\/871816.871852"},{"key":"e_1_3_2_69_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10672-9_11"},{"key":"e_1_3_2_70_2","doi-asserted-by":"publisher","DOI":"10.1145\/1379022.1375583"},{"key":"e_1_3_2_71_2","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2015.77"},{"key":"e_1_3_2_72_2","unstructured":"Sebastian Ullrich. 2016. Electrolysis Reference. Retrieved from http:\/\/kha.github.io\/electrolysis\/."},{"key":"e_1_3_2_75_2","doi-asserted-by":"publisher","DOI":"10.1145\/321978.321991"},{"key":"e_1_3_2_76_2","unstructured":"Z3 Team. 2021. The Z3 Theorem Prover. Retrieved from https:\/\/github.com\/Z3Prover\/z3."}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3462205","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3462205","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:48:53Z","timestamp":1750193333000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3462205"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,31]]},"references-count":70,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2021,12,31]]}},"alternative-id":["10.1145\/3462205"],"URL":"https:\/\/doi.org\/10.1145\/3462205","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,10,31]]},"assertion":[{"value":"2020-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-10-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}