{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:44:03Z","timestamp":1775868243051,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":46,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,6,9]],"date-time":"2022-06-09T00:00:00Z","timestamp":1654732800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,6,9]]},"DOI":"10.1145\/3519939.3523704","type":"proceedings-article","created":{"date-parts":[[2022,6,2]],"date-time":"2022-06-02T21:05:05Z","timestamp":1654203905000},"page":"841-856","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":40,"title":["RustHornBelt: a semantic foundation for functional verification of Rust programs with unsafe code"],"prefix":"10.1145","author":[{"given":"Yusuke","family":"Matsushita","sequence":"first","affiliation":[{"name":"University of Tokyo, Japan"}]},{"given":"Xavier","family":"Denis","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris-Saclay, France \/ CNRS, France \/ ENS Paris-Saclay, France \/ Inria, France \/ Laboratoire M\u00e9thodes Formelles, France"}]},{"given":"Jacques-Henri","family":"Jourdan","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Paris-Saclay, France \/ CNRS, France \/ ENS Paris-Saclay, France \/ Inria, France \/ Laboratoire M\u00e9thodes Formelles, France"}]},{"given":"Derek","family":"Dreyer","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}]}],"member":"320","published-online":{"date-parts":[[2022,6,9]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1988.5115"},{"key":"e_1_3_2_1_2_1","volume-title":"Semantics of Types for Mutable State. Ph. D. Dissertation","author":"Ahmed Amal","unstructured":"Amal Ahmed . 2004. Semantics of Types for Mutable State. Ph. D. Dissertation . Princeton University . Amal Ahmed. 2004. Semantics of Types for Mutable State. Ph. D. Dissertation. Princeton University."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1709093.1709094"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932501"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360573"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158093"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23534-9_2"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411235"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/286936.286947"},{"key":"e_1_3_2_1_12_1","unstructured":"Coq Community. 2021. The Coq Proof Assistant. https:\/\/coq.inria.fr\/  Coq Community. 2021. The Coq Proof Assistant. https:\/\/coq.inria.fr\/"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371101"},{"key":"e_1_3_2_1_15_1","unstructured":"Xavier Denis Jacques-Henri Jourdan and Claude March\u00e9. 2021. The Creusot Environment for the Deductive Verification of Rust Programs. https:\/\/hal.inria.fr\/hal-03526634  Xavier Denis Jacques-Henri Jourdan and Claude March\u00e9. 2021. The Creusot Environment for the Deductive Verification of Rust Programs. https:\/\/hal.inria.fr\/hal-03526634"},{"key":"e_1_3_2_1_16_1","volume-title":"A Discipline of Programming","author":"Dijkstra Edsger W.","year":"1958","unstructured":"Edsger W. Dijkstra . 1976. A Discipline of Programming . Prentice-Hall . isbn:013215871X https:\/\/www.worldcat.org\/oclc\/0 1958 445 Edsger W. Dijkstra. 1976. A Discipline of Programming. Prentice-Hall. isbn:013215871X https:\/\/www.worldcat.org\/oclc\/01958445"},{"key":"e_1_3_2_1_17_1","unstructured":"Dropbox. 2020. Rewriting the Heart of Our Sync Engine - Dropbox. https:\/\/dropbox.tech\/infrastructure\/rewriting-the-heart-of-our-sync-engine  Dropbox. 2020. Rewriting the Heart of Our Sync Engine - Dropbox. https:\/\/dropbox.tech\/infrastructure\/rewriting-the-heart-of-our-sync-engine"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_3_2_1_19_1","unstructured":"Google. 2021. Rust in the Android platform. https:\/\/security.googleblog.com\/2021\/04\/rust-in-android-platform.html  Google. 2021. Rust in the Android platform. https:\/\/security.googleblog.com\/2021\/04\/rust-in-android-platform.html"},{"key":"e_1_3_2_1_20_1","volume-title":"Understanding and Evolving the Rust Programming Language. Ph. D. Dissertation","author":"Jung Ralf","year":"1880","unstructured":"Ralf Jung . 2020. Understanding and Evolving the Rust Programming Language. Ph. D. Dissertation . Saarland University , Saarbr\u00fccken, Germany . https:\/\/publikationen.sulb.uni-saarland.de\/handle\/20.500.1 1880 \/29647 Ralf Jung. 2020. Understanding and Evolving the Rust Programming Language. Ph. D. Dissertation. Saarland University, Saarbr\u00fccken, Germany. https:\/\/publikationen.sulb.uni-saarland.de\/handle\/20.500.11880\/29647"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3418295"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371113"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_2_1_26_1","volume-title":"Proceedings of the ACM on Programming Languages, 1.","author":"Sharon Shoham Hari Govind V K","year":"2022","unstructured":"Hari Govind V K , Sharon Shoham , and Arie Gurfinkel . 2022 . Solving Constrained Horn Clauses Modulo Algebraic Data Types and Recursive Functions . Proceedings of the ACM on Programming Languages, 1. Hari Govind V K, Sharon Shoham, and Arie Gurfinkel. 2022. Solving Constrained Horn Clauses Modulo Algebraic Data Types and Recursive Functions. Proceedings of the ACM on Programming Languages, 1."},{"key":"e_1_3_2_1_27_1","unstructured":"Steve Klabnik Carol Nichols and Rust Community. 2018. The Rust Programming Language. https:\/\/doc.rust-lang.org\/book\/  Steve Klabnik Carol Nichols and Rust Community. 2018. The Rust Programming Language. https:\/\/doc.rust-lang.org\/book\/"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462189"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2663171.2663188"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.6501665"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_18"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3462205"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_1"},{"key":"e_1_3_2_1_35_1","unstructured":"Mozilla. 2021. Rust language \u2014 Mozilla Research. https:\/\/research.mozilla.org\/rust\/  Mozilla. 2021. Rust language \u2014 Mozilla Research. https:\/\/research.mozilla.org\/rust\/"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_3_2_1_37_1","unstructured":"npm. 2019. Rust Case Study: Community Makes Rust an Easy Choice for npm. https:\/\/www.rust-lang.org\/static\/pdfs\/Rust-npm-Whitepaper.pdf  npm. 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_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_3_2_1_39_1","unstructured":"Rust Community. 2021. Rust Programming Language. https:\/\/www.rust-lang.org\/  Rust Community. 2021. Rust Programming Language. https:\/\/www.rust-lang.org\/"},{"key":"e_1_3_2_1_40_1","unstructured":"Rust Community. 2021. Sponsors \u2014 Rust Programming Language. https:\/\/www.rust-lang.org\/sponsors  Rust Community. 2021. Sponsors \u2014 Rust Programming Language. https:\/\/www.rust-lang.org\/sponsors"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454031"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429111"},{"key":"e_1_3_2_1_43_1","volume-title":"Simple Verification of Rust Programs via Functional Purification. Master\u2019s thesis","author":"Ullrich Sebastian","unstructured":"Sebastian Ullrich . 2016. Simple Verification of Rust Programs via Functional Purification. Master\u2019s thesis . Karlsruhe Institute of Technology . https:\/\/pp.ipd.kit.edu\/uploads\/publikationen\/ullrich16masterarbeit.pdf Sebastian Ullrich. 2016. Simple Verification of Rust Programs via Functional Purification. Master\u2019s thesis. Karlsruhe Institute of Technology. https:\/\/pp.ipd.kit.edu\/uploads\/publikationen\/ullrich16masterarbeit.pdf"},{"key":"e_1_3_2_1_44_1","volume-title":"Modular Fine-Grained Concurrency Verification. Ph. D. Dissertation","author":"Vafeiadis Viktor","unstructured":"Viktor Vafeiadis . 2008. Modular Fine-Grained Concurrency Verification. Ph. D. Dissertation . University of Cambridge , UK. http:\/\/ethos.bl.uk\/OrderDetails.do?uin=uk.bl.ethos.612221 Viktor Vafeiadis. 2008. Modular Fine-Grained Concurrency Verification. Ph. D. Dissertation. University of Cambridge, UK. http:\/\/ethos.bl.uk\/OrderDetails.do?uin=uk.bl.ethos.612221"},{"issue":"2","key":"e_1_3_2_1_45_1","first-page":"2","article-title":"Linear Types Can Change the World!. In Programming concepts and methods","volume":"2","author":"Wadler Philip","year":"1990","unstructured":"Philip Wadler . 1990 . Linear Types Can Change the World!. In Programming concepts and methods : Proceedings of the IFIP Working Group 2 . 2 , 2 .3 Working Conference on Programming Concepts and Methods, Manfred Broy (Ed.). North-Holland, 561. isbn:0-444-88545-5 Philip Wadler. 1990. Linear Types Can Change the World!. In Programming concepts and methods: Proceedings of the IFIP Working Group 2.2, 2.3 Working Conference on Programming Concepts and Methods, Manfred Broy (Ed.). North-Holland, 561. isbn:0-444-88545-5","journal-title":"Proceedings of the IFIP Working Group"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29952-0_12"}],"event":{"name":"PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation","location":"San Diego CA USA","acronym":"PLDI '22","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3519939.3523704","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3519939.3523704","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:10:30Z","timestamp":1750183830000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3519939.3523704"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,6,9]]},"references-count":46,"alternative-id":["10.1145\/3519939.3523704","10.1145\/3519939"],"URL":"https:\/\/doi.org\/10.1145\/3519939.3523704","relation":{},"subject":[],"published":{"date-parts":[[2022,6,9]]},"assertion":[{"value":"2022-06-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}