{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,2]],"date-time":"2025-08-02T14:29:21Z","timestamp":1754144961777,"version":"3.41.2"},"reference-count":72,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","funder":[{"name":"JSPS KAKENHI","award":["JP20H04162,JP20H05703,JP20H00582,JP22H03564,JP23K24826,JP24H00699,JP25H00446"],"award-info":[{"award-number":["JP20H04162,JP20H05703,JP20H00582,JP22H03564,JP23K24826,JP24H00699,JP25H00446"]}]},{"name":"JST CREST","award":["JPMJCR21M3"],"award-info":[{"award-number":["JPMJCR21M3"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,6,10]]},"abstract":"<jats:p>\n            We introduce Thrust, a new verification tool for ensuring functional correctness in Rust, distinguished by its strengths in\n            <jats:italic toggle=\"yes\">automated<\/jats:italic>\n            verification, including the synthesis of inductive invariants for loops and recursive functions. Thrust is built on a novel dependent refinement type system for Rust and refinement type inference techniques based on Constrained Horn Clause (CHC) solvers. Leveraging advantages of the type system, Thrust also supports semi-automated verification utilizing user type annotations to complement CHC solvers in cases where automatic constraint solving is unsuccessful, as well as\n            <jats:italic toggle=\"yes\">modular<\/jats:italic>\n            verification at the function and subexpression levels. Thrust also achieves\n            <jats:italic toggle=\"yes\">precise<\/jats:italic>\n            verification, especially for programs involving pointer aliasing and borrowing, without sacrificing the benefits of automated verification, by incorporating the notion of\n            <jats:italic toggle=\"yes\">prophecy<\/jats:italic>\n            into the refinement type system: it not only enables strong updates by leveraging the \u201caliasing XOR mutability\u201d guarantee provided by Rust\u2019s type system, but also achieves propagation of update information to the original owner upon mutable borrow release through the use of a prophecy variable. Incorporating prophecy into a refinement type system is itself challenging and requires certain tricks, as discussed in this paper, making a theoretical contribution and paving the way for further research into prophecy-based refinement type systems. While our type system addresses the challenge, we keep it simple for extensibility, specifically by delegating the guarantee of \u201caliasing XOR mutability,\u201d and, more technically, the \u201cwell-borrowedness\u201d of the program in the sense of the\n            <jats:italic toggle=\"yes\">stacked borrows<\/jats:italic>\n            aliasing model, to Rust\u2019s type system, allowing us to focus on reasoning about functional correctness and propagating update information through prophecy variables. Compared to RustHorn, another automated verification tool based on prophecy, our approach leverages the strengths of refinement types to support modular verification, higher-order functions, and refinement of data stored in algebraic data structures. We implemented Thrust, a refinement type inference tool as a plugin for the Rust compiler, and evaluated it using RustHorn benchmarks, as well as additional new benchmarks, including those that are beyond the capabilities of RustHorn and other semi-automated verification tools, obtaining promising results.\n          <\/jats:p>","DOI":"10.1145\/3729333","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"2056-2080","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Thrust: A Prophecy-Based Refinement Type System for Rust"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-0372-4863","authenticated-orcid":false,"given":"Hiromi","family":"Ogawa","sequence":"first","affiliation":[{"name":"University of Tsukuba, Tsukuba, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9286-230X","authenticated-orcid":false,"given":"Taro","family":"Sekiyama","sequence":"additional","affiliation":[{"name":"National Institute of Informatics, Tokyo, Japan"},{"name":"SOKENDAI, Hayama, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4225-8195","authenticated-orcid":false,"given":"Hiroshi","family":"Unno","sequence":"additional","affiliation":[{"name":"Tohoku University, Sendai, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","unstructured":"M. Abadi and L. Lamport. 1988. The existence of refinement mappings. In LICS \u201988. 165\u2013175. https:\/\/doi.org\/10.1109\/LICS.1988.5115 10.1109\/LICS.1988.5115","DOI":"10.1109\/LICS.1988.5115"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360573"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_3"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01090-4_32"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1890028.1890031"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","unstructured":"R. Beutner and B. Finkbeiner. 2022. Prophecy Variables for Hyperproperty Verification. In CSF \u201922. IEEE 471\u2013485. https:\/\/doi.org\/10.1109\/CSF54842.2022.9919658 10.1109\/CSF54842.2022.9919658","DOI":"10.1109\/CSF54842.2022.9919658"},{"volume-title":"International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO).","author":"B\u00edl\u00fd A.","key":"e_1_2_2_7_1","unstructured":"A. B\u00edl\u00fd, J. Hansen, P. M\u00fcller, and A. J. Summers. 2023. Compositional Reasoning about Advanced Iterator Patterns in Rust. In International Workshop on Aliasing, Confinement and Ownership in object-oriented programming (IWACO)."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23534-9_2"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_4"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"e_1_2_2_11_1","unstructured":"Rust Community. 2017. 2025-nested-method-calls - The Rust RFC Book. https:\/\/rust-lang.github.io\/rfcs\/2025-nested-method-calls.html"},{"key":"e_1_2_2_12_1","unstructured":"Rust Community. 2017. 2094-nll - The Rust RFC Book. https:\/\/rust-lang.github.io\/rfcs\/2094-nll.html"},{"key":"e_1_2_2_13_1","unstructured":"Rust Community. 2024. Rust Programming Language. https:\/\/www.rust-lang.org\/"},{"key":"e_1_2_2_14_1","unstructured":"Rust Community. 2024. The MIR (Mid-level IR) - Rust Compiler Development Guide. https:\/\/rustc-dev-guide.rust-lang.org\/mir\/index.html"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17244-1_6"},{"key":"e_1_2_2_16_1","unstructured":"The Rust Project Developers. 2019. Rust Case Study: Community Makes Rust an Easy Choice for npm. https:\/\/www.rust-lang.org\/static\/pdfs\/Rust-npm-Whitepaper.pdf"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40627-0_24"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/2157654.2157675"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.34727\/2022\/isbn.978-3-85448-053-2_45"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45251-6_29"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113468"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656422"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.23"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","unstructured":"Colin S. Gordon Michael D. Ernst and Dan Grossman. 2013. Rely-guarantee references for refinement types over aliased mutable data. In PLDI \u201913 (PLDI \u201913). ACM 73\u201384. https:\/\/doi.org\/10.1145\/2491956.2462160 10.1145\/2491956.2462160","DOI":"10.1145\/2491956.2462160"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674640"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547647"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_20"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371109"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371113"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_19"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3633280"},{"key":"e_1_2_2_36_1","doi-asserted-by":"crossref","unstructured":"Naoki Kobayashi Ryosuke Sato and Hiroshi Unno. 2011. Predicate abstraction and CEGAR for higher-order model checking. In PLDI \u201911. ACM 222\u2013233.","DOI":"10.1145\/1993498.1993525"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_2"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_7"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674662"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586037"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591283"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/INDIN.2018.8471992"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-18(3:26)2022"},{"key":"e_1_2_2_44_1","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 \u201922. ACM 841\u2013856. https:\/\/doi.org\/10.1145\/3519939.3523704 10.1145\/3519939.3523704","DOI":"10.1145\/3519939.3523704"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3462205"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-50521-8_11"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","unstructured":"Yoji Nanjo Hiroshi Unno Eric Koskinen and Tachio Terauchi. 2018. A Fixpoint Logic and Dependent Effects for Temporal Property Verification. In LICS \u201918. ACM 759\u2013768. https:\/\/doi.org\/10.1145\/3209108.3209204 10.1145\/3209108.3209204","DOI":"10.1145\/3209108.3209204"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.15260858"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","unstructured":"Patrick Rondon Ming Kawaguchi and Ranjit Jhala. 2008. Liquid Types. In PLDI \u201908. ACM 159\u2013169. https:\/\/doi.org\/10.1145\/1375581.1375602 10.1145\/1375581.1375602","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","unstructured":"Patrick Maxim Rondon Ming Kawaguchi and Ranjit Jhala. 2010. Low-level liquid types. In POPL \u201910. ACM 131\u2013144. https:\/\/doi.org\/10.1145\/1706299.1706316 10.1145\/1706299.1706316","DOI":"10.1145\/1706299.1706316"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571264"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46425-5_24"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","unstructured":"Nikhil Swamy Joel Weinberger Cole Schlesinger Juan Chen and Benjamin Livshits. 2013. Verifying higher-order programs with the dijkstra monad. In PLDI \u201913 (PLDI \u201913). ACM 387\u2013398. https:\/\/doi.org\/10.1145\/2491956.2491978 10.1145\/2491956.2491978","DOI":"10.1145\/2491956.2491978"},{"key":"e_1_2_2_56_1","unstructured":"The Rust Compiler Team. 2022. The Polonius Book. https:\/\/rust-lang.github.io\/polonius\/"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2015.77"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_25"},{"key":"e_1_2_2_59_1","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"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656457"},{"key":"e_1_2_2_61_1","unstructured":"Sebastian Andreas Ullrich. 2016. Simple Verification of Rust Programs via Functional Purification. https:\/\/pp.ipd.kit.edu\/uploads\/publikationen\/ullrich16masterarbeit.pdf"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","unstructured":"Hiroshi Unno and Naoki Kobayashi. 2009. Dependent Type Inference with Interpolants. In PPDP \u201909. ACM 277\u2013288. https:\/\/doi.org\/10.1145\/1599410.1599445 10.1145\/1599410.1599445","DOI":"10.1145\/1599410.1599445"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158100"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","unstructured":"Hiroshi Unno Tachio Terauchi and Naoki Kobayashi. 2013. Automating Relatively Complete Verification of Higher-order Functional Programs. In POPL \u201913. ACM 75\u201386. https:\/\/doi.org\/10.1145\/2429069.2429081 10.1145\/2429069.2429081","DOI":"10.1145\/2429069.2429081"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_35"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","unstructured":"Alexa VanHattum Daniel Schwartz-Narbonne Nathan Chong and Adrian Sampson. 2022. Verifying dynamic trait objects in Rust. ICSE-SEIP \u201922. ACM 321\u2013330. https:\/\/doi.org\/10.1145\/3510457.3513031 10.1145\/3510457.3513031","DOI":"10.1145\/3510457.3513031"},{"key":"e_1_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485522"},{"key":"e_1_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932500"},{"key":"e_1_2_2_71_1","doi-asserted-by":"publisher","unstructured":"Hongwei Xi and Frank Pfenning. 1998. Eliminating array bound checking through dependent types. In PLDI \u201998. ACM 249\u2013257. https:\/\/doi.org\/10.1145\/277650.277732 10.1145\/277650.277732","DOI":"10.1145\/277650.277732"},{"key":"e_1_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/b105205"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729333","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,16]],"date-time":"2025-07-16T06:05:42Z","timestamp":1752645942000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729333"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":72,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729333"],"URL":"https:\/\/doi.org\/10.1145\/3729333","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}