{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:12:02Z","timestamp":1775790722573,"version":"3.50.1"},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T00:00:00Z","timestamp":1686009600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["Grant No. 191114"],"award-info":[{"award-number":["Grant No. 191114"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Singapore Ministry of Education","award":["Tier 3 grant Automated Program Repair, MOE-MOET32021-0001"],"award-info":[{"award-number":["Tier 3 grant Automated Program Repair, MOE-MOET32021-0001"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,6,6]]},"abstract":"<jats:p>The Rust type system guarantees memory safety and data-race freedom. However, to satisfy Rust's type rules, many familiar implementation patterns must be adapted substantially. These necessary adaptations complicate programming and might hinder language adoption. In this paper, we demonstrate that, in contrast to manual programming, automatic synthesis is not complicated by Rust's type system, but rather benefits in two major ways. First, a Rust synthesizer can get away with significantly simpler specifications. While in more traditional imperative languages, synthesizers often require lengthy annotations in a complex logic to describe the shape of data structures, aliasing, and potential side effects, in Rust, all this information can be inferred from the types, letting the user focus on specifying functional properties using a slight extension of Rust expressions. Second, the Rust type system reduces the search space for synthesis, which improves performance.<\/jats:p>\n          <jats:p>In this work, we present the first approach to automatically synthesizing correct-by-construction programs in safe Rust. The key ingredient of our synthesis procedure is Synthetic Ownership Logic, a new program logic for deriving programs that are guaranteed to satisfy both a user-provided functional specification and, importantly, Rust's intricate type system. We implement this logic in a new tool called RusSOL. Our evaluation shows the effectiveness of RusSOL, both in terms of annotation burden and performance, in synthesizing provably correct solutions to common problems faced by new Rust developers.<\/jats:p>","DOI":"10.1145\/3591278","type":"journal-article","created":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T20:06:24Z","timestamp":1686081984000},"page":"1414-1437","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Leveraging Rust Types for Program Synthesis"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-2121-7044","authenticated-orcid":false,"given":"Jon\u00e1\u0161","family":"Fiala","sequence":"first","affiliation":[{"name":"ETH Zurich, Switzerland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7276-7644","authenticated-orcid":false,"given":"Shachar","family":"Itzhaky","sequence":"additional","affiliation":[{"name":"Technion, Israel"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7001-2566","authenticated-orcid":false,"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5571-173X","authenticated-orcid":false,"given":"Nadia","family":"Polikarpova","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4250-5392","authenticated-orcid":false,"given":"Ilya","family":"Sergey","sequence":"additional","affiliation":[{"name":"National University of Singapore, Singapore"}]}],"member":"320","published-online":{"date-parts":[[2023,6,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1988.5115"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360573"},{"key":"e_1_2_1_3_1","unstructured":"Aria Beingessner. 2015. Learning Rust With Entirely Too Many Linked Lists. https:\/\/rust-unofficial.github.io\/too-many-lists\/ \t\t\t\t  Aria Beingessner. 2015. Learning Rust With Entirely Too Many Linked Lists. https:\/\/rust-unofficial.github.io\/too-many-lists\/"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36946-9_10"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_6"},{"key":"e_1_2_1_6_1","unstructured":"Xavier Denis Jacques-Henri Jourdan and Claude March\u00e9. 2021. The CREUSOT Environment for the Deductive Verification of Rust Programs. Inria Saclay - \u00cele de France. https:\/\/hal.inria.fr\/hal-03526634 \t\t\t\t  Xavier Denis Jacques-Henri Jourdan and Claude March\u00e9. 2021. The CREUSOT Environment for the Deductive Verification of Rust Programs. Inria Saclay - \u00cele de France. https:\/\/hal.inria.fr\/hal-03526634"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7811786"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547647"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454087"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_5"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371109"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509555"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586037"},{"key":"e_1_2_1_15_1","volume-title":"Proc. ACM Program. Lang., 7, PLDI","author":"Lehmann Nico","year":"2023","unstructured":"Nico Lehmann , Adam Geller , Niki Vazou , and Ranjit Jhala . 2023 . Flux: Liquid Types for Rust . Proc. ACM Program. Lang., 7, PLDI (2023), To appear. Nico Lehmann, Adam Geller, Niki Vazou, and Ranjit Jhala. 2023. Flux: Liquid Types for Rust. Proc. ACM Program. Lang., 7, PLDI (2023), To appear."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/357084.357090"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2663171.2663188"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523704"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3462205"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290385"},{"key":"e_1_2_1_23_1","unstructured":"The Rust Team. 2017. The Rust programming language.  http:\/\/rust-lang.org \t\t\t\t  The Rust Team. 2017. The Rust programming language.  http:\/\/rust-lang.org"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13464-7_14"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454084"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99404"},{"key":"e_1_2_1_27_1","volume-title":"Oxide: The Essence of Rust. CoRR, abs\/1903.00982","author":"Weiss Aaron","year":"2019","unstructured":"Aaron Weiss , Daniel Patterson , Nicholas D. Matsakis , and Amal Ahmed . 2019 . Oxide: The Essence of Rust. CoRR, abs\/1903.00982 (2019), arXiv:1903.00982. arxiv:1903.00982 Aaron Weiss, Daniel Patterson, Nicholas D. Matsakis, and Amal Ahmed. 2019. Oxide: The Essence of Rust. CoRR, abs\/1903.00982 (2019), arXiv:1903.00982. arxiv:1903.00982"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485522"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591278","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3591278","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:47:20Z","timestamp":1750178840000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591278"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,6]]},"references-count":28,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2023,6,6]]}},"alternative-id":["10.1145\/3591278"],"URL":"https:\/\/doi.org\/10.1145\/3591278","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,6,6]]},"assertion":[{"value":"2023-06-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}