{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,8]],"date-time":"2026-10-08T11:34:43Z","timestamp":1791459283777,"version":"4.3.4"},"reference-count":50,"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":"NSF","doi-asserted-by":"publisher","award":["CNS-2120642, CNS-2155235, CCF-1918573, CCF-1911213"],"award-info":[{"award-number":["CNS-2120642, CNS-2155235, CCF-1918573, CCF-1911213"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100019180","name":"HORIZON EUROPE European Research Council","doi-asserted-by":"publisher","award":["GA: 101039196"],"award-info":[{"award-number":["GA: 101039196"]}],"id":[{"id":"10.13039\/100019180","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["Ref. N00014-19-1-2292"],"award-info":[{"award-number":["Ref. N00014-19-1-2292"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]}],"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>We introduce Flux, which shows how logical refinements can work hand in glove with Rust's ownership mechanisms to yield ergonomic type-based verification of low-level pointer manipulating programs. First, we design a novel refined type system for Rust that indexes mutable locations, with pure (immutable) values that can appear in refinements, and then exploits Rust's ownership mechanisms to abstract sub-structural reasoning about locations within Rust's polymorphic type constructors, while supporting strong updates. We formalize the crucial dependency upon Rust's strong aliasing guarantees by exploiting the Stacked Borrows aliasing model to prove that \"well-borrowed evaluations of well-typed programs do not get stuck\". Second, we implement our type system in Flux, a plug-in to the Rust compiler that exploits the factoring of complex invariants into types and refinements to efficiently synthesize loop annotations-including complex quantified invariants describing the contents of containers-via liquid inference. Third, we evaluate Flux with a benchmark suite of vector manipulating programs and parts of a previously verified secure sandboxing library to demonstrate the advantages of refinement types over program logics as implemented in the state-of-the-art Prusti verifier. While Prusti's more expressive program logic can, in general, verify deep functional correctness specifications, for the lightweight but ubiquitous and important verification use-cases covered by our benchmarks, liquid typing makes verification ergonomic by slashing specification lines by a factor of two, verification time by an order of magnitude, and annotation overhead from up to 24% of code size (average 14%), to nothing at all.<\/jats:p>","DOI":"10.1145\/3591283","type":"journal-article","created":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T20:06:24Z","timestamp":1686081984000},"page":"1533-1557","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":38,"title":["Flux: Liquid Types for Rust"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-6838-3714","authenticated-orcid":false,"given":"Nico","family":"Lehmann","sequence":"first","affiliation":[{"name":"University of California at San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-8137-7577","authenticated-orcid":false,"given":"Adam T.","family":"Geller","sequence":"additional","affiliation":[{"name":"University of British Columbia, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0732-5476","authenticated-orcid":false,"given":"Niki","family":"Vazou","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1802-9421","authenticated-orcid":false,"given":"Ranjit","family":"Jhala","sequence":"additional","affiliation":[{"name":"University of California at San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,6,6]]},"reference":[{"key":"e_1_2_1_1_1","first-page":"397","article-title":"L^3: a linear language with locations","volume":"77","author":"Ahmed Amal","year":"2007","unstructured":"Amal Ahmed , Matthew Fluet , and Greg Morrisett . 2007 . L^3: a linear language with locations . Fundamenta Informaticae , 77 , 4 (2007), 397 \u2013 449 . Amal Ahmed, Matthew Fluet, and Greg Morrisett. 2007. L^3: a linear language with locations. Fundamenta Informaticae, 77, 4 (2007), 397\u2013449.","journal-title":"Fundamenta Informaticae"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511609619"},{"key":"e_1_2_1_3_1","volume-title":"Summers","author":"Astrauskas Vytautas","year":"2022","unstructured":"Vytautas Astrauskas , Aurel B\u00edl\u00fd , Jon\u00e1\u0161 Fiala , Zachary Grannan , Christoph Matheja , Peter M\u00fcller , Federico Poli , and Alexander J . Summers . 2022 . The Prusti Project: Formal Verification for\u00a0Rust. In NASA Formal Methods, Jyotirmoy V. Deshmukh, Klaus Havelund, and Ivan Perez (Eds.). Springer International Publishing , Cham. 88\u2013108. isbn:978-3-031-06773-0 https:\/\/link.springer.com\/chapter\/10.1007\/978-3-031-06773-0_5 Vytautas Astrauskas, Aurel B\u00edl\u00fd, Jon\u00e1\u0161 Fiala, Zachary Grannan, Christoph Matheja, Peter M\u00fcller, Federico Poli, and Alexander J. Summers. 2022. The Prusti Project: Formal Verification for\u00a0Rust. In NASA Formal Methods, Jyotirmoy V. Deshmukh, Klaus Havelund, and Ivan Perez (Eds.). Springer International Publishing, Cham. 88\u2013108. isbn:978-3-031-06773-0 https:\/\/link.springer.com\/chapter\/10.1007\/978-3-031-06773-0_5"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360573"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_3"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3139645.3139660"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23534-9_2"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36946-9_3"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/286936.286947"},{"key":"e_1_2_1_10_1","unstructured":"R. L. Constable and S. F. Smith. 1987. Partial Objects In Constructive Type Theory. In LICS. R. L. Constable and S. F. Smith. 1987. Partial Objects In Constructive Type Theory. In LICS."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110270"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17244-1_6"},{"key":"e_1_2_1_14_1","doi-asserted-by":"crossref","unstructured":"Dimitrios J Economou Neel Krishnaswami and Jana Dunfield. 2022. Focusing on Liquid Refinement Typing. arXiv preprint arXiv:2209.13000. Dimitrios J Economou Neel Krishnaswami and Jana Dunfield. 2022. Focusing on Liquid Refinement Typing. arXiv preprint arXiv:2209.13000.","DOI":"10.1145\/3610408"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113468"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547647"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000032"},{"key":"e_1_2_1_19_1","volume-title":"WaVe: A Verifiably Secure WebAssembly Sandboxing Runtime. In 2023 IEEE Symposium on Security and Privacy (SP). IEEE Computer Society","author":"Johnson E.","year":"1986","unstructured":"E. Johnson , E. Laufer , Z. Zhao , D. Gohman , S. Narayan , S. Savage , D. Stefan , and F. Brown . 2023 . WaVe: A Verifiably Secure WebAssembly Sandboxing Runtime. In 2023 IEEE Symposium on Security and Privacy (SP). IEEE Computer Society , Los Alamitos, CA, USA. 1986 \u20132001. https:\/\/doi.org\/10.1109\/SP46215.2023.00114 10.1109\/SP46215.2023.00114 E. Johnson, E. Laufer, Z. Zhao, D. Gohman, S. Narayan, S. Savage, D. Stefan, and F. Brown. 2023. WaVe: A Verifiably Secure WebAssembly Sandboxing Runtime. In 2023 IEEE Symposium on Security and Privacy (SP). IEEE Computer Society, Los Alamitos, CA, USA. 1986\u20132001. https:\/\/doi.org\/10.1109\/SP46215.2023.00114"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371109"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254071"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2015.396"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7682468"},{"key":"e_1_2_1_26_1","volume-title":"Flux: Liquid Types for Rust - Technical Appendix. https:\/\/github.com\/flux-rs\/pldi23-artifact","author":"Lehmann Nico","year":"2023","unstructured":"Nico Lehmann , Adam T. Geller , Niki Vazou , and Ranjit Jhala . 2023 . Flux: Liquid Types for Rust - Technical Appendix. https:\/\/github.com\/flux-rs\/pldi23-artifact Nico Lehmann, Adam T. Geller, Niki Vazou, and Ranjit Jhala. 2023. Flux: Liquid Types for Rust - Technical Appendix. https:\/\/github.com\/flux-rs\/pldi23-artifact"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_20"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/INDIN.2018.8471992"},{"key":"e_1_2_1_29_1","unstructured":"Niko Matsakis. 2018. An alias-based formulation of the borrow checker. https:\/\/smallcultfollowing.com\/babysteps\/blog\/2018\/04\/27\/an-alias-based-formulation-of-the-borrow-checker\/ Niko Matsakis. 2018. An alias-based formulation of the borrow checker. https:\/\/smallcultfollowing.com\/babysteps\/blog\/2018\/04\/27\/an-alias-based-formulation-of-the-borrow-checker\/"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2692956.2663188"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3462205"},{"key":"e_1_2_1_32_1","unstructured":"Denis Merigoux Franziskus Kiefer and Karthikeyan Bhargavan. 2021. Hacspec: succinct executable verifiable specifications for high-assurance cryptography embedded in Rust. Ph. D. Dissertation. Inria. Denis Merigoux Franziskus Kiefer and Karthikeyan Bhargavan. 2021. Hacspec: succinct executable verifiable specifications for high-assurance cryptography embedded in Rust. Ph. D. Dissertation. Inria."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054091"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-28644-8_4"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706316"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.713327"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46425-5_24"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-44914-8_25"},{"key":"e_1_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 , Karlsruher Institut f\u00fcr Technologie (KIT) . Sebastian Ullrich. 2016. Simple verification of rust programs via functional purification. Master\u2019s Thesis, Karlsruher Institut f\u00fcr Technologie (KIT)."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3510457.3513031"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158141"},{"key":"e_1_2_1_46_1","volume-title":"Oxide: The essence of rust. arXiv preprint arXiv:1903.00982.","author":"Weiss Aaron","year":"2019","unstructured":"Aaron Weiss , Olek Gierczak , Daniel Patterson , and Amal Ahmed . 2019 . Oxide: The essence of rust. arXiv preprint arXiv:1903.00982. Aaron Weiss, Olek Gierczak, Daniel Patterson, and Amal Ahmed. 2019. Oxide: The essence of rust. arXiv preprint arXiv:1903.00982."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24849-1_25"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292560"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292560"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30557-6_8"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591283","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3591283","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\/3591283"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,6]]},"references-count":50,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2023,6,6]]}},"alternative-id":["10.1145\/3591283"],"URL":"https:\/\/doi.org\/10.1145\/3591283","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"}}]}}