{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:05:06Z","timestamp":1784199906040,"version":"3.55.0"},"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\n                    <jats:sc>Thrust<\/jats:sc>\n                    , a new verification tool for ensuring functional correctness in\n                    <jats:sc>Rust<\/jats:sc>\n                    , 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.\n                    <jats:sc>Thrust<\/jats:sc>\n                    is built on a novel dependent refinement type system for\n                    <jats:sc>Rust<\/jats:sc>\n                    and refinement type inference techniques based on Constrained Horn Clause (CHC) solvers. Leveraging advantages of the type system,\n                    <jats:sc>Thrust<\/jats:sc>\n                    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.\n                    <jats:sc>Thrust<\/jats:sc>\n                    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\n                    <jats:sc>Rust<\/jats:sc>\n                    \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<\/jats:italic>\n                    borrows aliasing model, to\n                    <jats:sc>Rust<\/jats:sc>\n                    \u2019s type system, allowing us to focus on reasoning about functional correctness and propagating update information through prophecy variables. Compared to\n                    <jats:sc>RustHorn<\/jats:sc>\n                    , 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\n                    <jats:sc>Thrust<\/jats:sc>\n                    , a refinement type inference tool as a plugin for the\n                    <jats:sc>Rust<\/jats:sc>\n                    compiler, and evaluated it using\n                    <jats:sc>RustHorn<\/jats:sc>\n                    benchmarks, as well as additional new benchmarks, including those that are beyond the capabilities of\n                    <jats:sc>RustHorn<\/jats:sc>\n                    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":[{"vocabulary":"crossref","role":"author"}]},{"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":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4225-8195","authenticated-orcid":false,"given":"Hiroshi","family":"Unno","sequence":"additional","affiliation":[{"name":"Tohoku University, Sendai, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","unstructured":"M. Abadi and L. Lamport. 1988. The existence of refinement mappings. In LICS \u201988. 165\u2013175. doi:10.1109\/LICS.1988.5115","DOI":"10.1109\/LICS.1988.5115"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/3360573"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_3"},{"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\/1890028.1890031"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF54842.2022.9919658"},{"key":"e_1_3_2_8_2","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_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23534-9_2"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_4"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"e_1_3_2_12_2","unstructured":"Rust Community. 2017. 2025-nested-method-calls - The Rust RFC Book. https:\/\/rust-lang.github.io\/rfcs\/2025-nestedmethod-calls.html."},{"key":"e_1_3_2_13_2","unstructured":"Rust Community. 2017. 2094-nll - The Rust RFC Book. https:\/\/rust-lang.github.io\/rfcs\/2094-nll.html."},{"key":"e_1_3_2_14_2","unstructured":"Rust Community. 2024. Rust Programming Language. https:\/\/www.rust-lang.org\/."},{"key":"e_1_3_2_15_2","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_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17244-1_6"},{"key":"e_1_3_2_17_2","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_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40627-0_24"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.5555\/2157654.2157675"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","unstructured":"Zafer Esen and Philipp R\u00fcmmer. 2022. Tricera: Verifying C Programs Using the Theory of Heaps. In FMCAD \u201922. 380\u2013391. doi:10.34727\/2022\/isbn.978-3-85448-053-2_45","DOI":"10.34727\/2022\/isbn.978-3-85448-053-2_45"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45251-6_29"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113468"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656422"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.23"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462160"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3674640"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/3547647"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_20"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371109"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371113"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_19"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3633280"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993525"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_2"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_7"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/3674662"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/3586037"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591283"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","unstructured":"Marcus Lindner Jorge Aparicius and Per Lindgren. 2018. No Panic! Verification of Rust Programs by Symbolic Execution. In 2018 IEEE 16th International Conference on Industrial Informatics (INDIN). 108\u2013114. doi:10.1109\/INDIN.2018.8471992","DOI":"10.1109\/INDIN.2018.8471992"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-18(3:26)2022"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523704"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/3462205"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-50521-8_11"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209204"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","unstructured":"Hiromi Ogawa Taro Sekiyama and Hiroshi Unno. 2025. Thrust: A Prophecy-based Refinement Type System for Rust - Artifact. doi:10.5281\/zenodo.15260858","DOI":"10.5281\/zenodo.15260858"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706316"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571264"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46425-5_24"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491978"},{"key":"e_1_3_2_57_2","unstructured":"The Rust Compiler Team. 2022. The Polonius Book. https:\/\/rust-lang.github.io\/polonius\/."},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","unstructured":"John Toman Stuart Pernsteiner and Emina Torlak. 2015. Crust: A Bounded Verifier for Rust (N). In 2015 30th IEEE\/ACM International Conference on Automated Software Engineering (ASE). 75\u201380. doi:10.1109\/ASE.2015.77","DOI":"10.1109\/ASE.2015.77"},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_25"},{"key":"e_1_3_2_60_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."},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656457"},{"key":"e_1_3_2_62_2","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_3_2_63_2","doi-asserted-by":"publisher","DOI":"10.1145\/1599410.1599445"},{"key":"e_1_3_2_64_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158100"},{"key":"e_1_3_2_65_2","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429081"},{"key":"e_1_3_2_66_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_35"},{"key":"e_1_3_2_67_2","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. doi:10.1145\/3510457.3513031","DOI":"10.1145\/3510457.3513031"},{"key":"e_1_3_2_68_2","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_3_2_69_2","doi-asserted-by":"publisher","DOI":"10.1145\/3485522"},{"key":"e_1_3_2_70_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_3_2_71_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932500"},{"key":"e_1_3_2_72_2","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277732"},{"key":"e_1_3_2_73_2","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":[[2026,7,16]],"date-time":"2026-07-16T10:05:26Z","timestamp":1784196326000},"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":[{"value":"2475-1421","type":"electronic"}],"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"}}]}}