{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T01:22:47Z","timestamp":1760059367896,"version":"build-2065373602"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","funder":[{"DOI":"10.13039\/501100000038","name":"Natural Sciences and Engineering Research Council of Canada","doi-asserted-by":"publisher","award":["RGPIN-2020-06072"],"award-info":[{"award-number":["RGPIN-2020-06072"]}],"id":[{"id":"10.13039\/501100000038","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":[[2025,10,9]]},"abstract":"<jats:p>Rust\u2019s novel type system has proved an attractive target for verification and program analysis tools, due to the rich guarantees it provides for controlling aliasing and mutability. However, fully understanding, extracting and exploiting these guarantees is subtle and challenging: existing models for Rust\u2019s type checking either support a smaller idealised language disconnected from real-world Rust code, or come with severe limitations in terms of precise modelling of Rust borrows, composite types storing them, function signatures and loops.<\/jats:p>\n          <jats:p>\n            In this paper, we present\n            <jats:italic toggle=\"yes\">Place Capability Graphs<\/jats:italic>\n            : a novel model of Rust\u2019s type-checking results, which lifts these limitations, and which can be directly calculated from the Rust compiler\u2019s own programmatic representations and analyses. We demonstrate that our model supports over 97% of Rust functions in the most popular public crates, and show its suitability as a general-purpose basis for verification and program analysis tools by developing promising new prototype versions of the existing Flowistry and Prusti tools.\n          <\/jats:p>","DOI":"10.1145\/3763122","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:49:50Z","timestamp":1759999790000},"page":"2002-2029","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Place Capability Graphs: A General-Purpose Model of Rust\u2019s Ownership and Borrowing Guarantees"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7042-7013","authenticated-orcid":false,"given":"Zachary","family":"Grannan","sequence":"first","affiliation":[{"name":"University of British Columbia, Vancouver, Canada"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9284-9161","authenticated-orcid":false,"given":"Aurel","family":"B\u00edl\u00fd","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-2121-7044","authenticated-orcid":false,"given":"Jon\u00e1\u0161","family":"Fiala","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-6839-2305","authenticated-orcid":false,"given":"Jasper","family":"Geer","sequence":"additional","affiliation":[{"name":"University of British Columbia, Vancouver, Canada"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-3285-5032","authenticated-orcid":false,"given":"Markus","family":"de Medeiros","sequence":"additional","affiliation":[{"name":"New York University, New York City, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7001-2566","authenticated-orcid":false,"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5554-9381","authenticated-orcid":false,"given":"Alexander J.","family":"Summers","sequence":"additional","affiliation":[{"name":"University of British Columbia, Vancouver, Canada"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360573"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477132.3483570"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1002\/SPE.370"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2016.5"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45070-2_9"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/286936.286947"},{"key":"e_1_2_1_7_1","volume-title":"Fast Actors. In International Workshop on Programming Based on Actors, Agents, and Decentralized Control. ACM, 1\u201312","author":"Clebsch Sylvan","year":"2015","unstructured":"Sylvan Clebsch, Sophia Drossopoulou, Sebastian Blessing, and Andy McNeil. 2015. Deny Capabilities for Safe, Fast Actors. In International Workshop on Programming Based on Actors, Agents, and Decentralized Control. ACM, 1\u201312."},{"key":"e_1_2_1_8_1","volume-title":"Place Expressions and Value Expressions (The Rust Reference). https:\/\/doc.rust-lang.org\/reference\/expressions.html##place-expressions-and-value-expressions Accessed","author":"Community Rust","year":"2025","unstructured":"Rust Community and Language Team. 2025. Place Expressions and Value Expressions (The Rust Reference). https:\/\/doc.rust-lang.org\/reference\/expressions.html##place-expressions-and-value-expressions Accessed July 2025"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622841"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523445"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17244-1_6"},{"key":"e_1_2_1_12_1","unstructured":"Prusti Developers. 2024-2025. Personal Communication."},{"key":"e_1_2_1_13_1","volume-title":"https:\/\/github.com\/prusti\/pcg Accessed","author":"Developers Prusti","year":"2025","unstructured":"Prusti Developers. 2025. PCG Repository. https:\/\/github.com\/prusti\/pcg Accessed August 21, 2025"},{"key":"e_1_2_1_14_1","volume-title":"Returning mutable references (discussion). https:\/\/github.com\/verus-lang\/verus\/discussions\/35 Accessed","author":"Developers Verus","year":"2025","unstructured":"Verus Developers. 2022. Returning mutable references (discussion). https:\/\/github.com\/verus-lang\/verus\/discussions\/35 Accessed March, 2025"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384619"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.16597989"},{"key":"e_1_2_1_17_1","volume-title":"Summers","author":"Grannan Zachary","year":"2025","unstructured":"Zachary Grannan, Aurel B\u00edl\u00fd, Jon\u00e1\u0161 Fiala, Jasper Geer, Markus de Medeiros, Peter M\u00fcller, and Alexander J. Summers. 2025. Place Capability Graphs: A General-Purpose Model of Rust\u2019s Ownership and Borrowing Guarantees. arxiv:2503.21691. arxiv:2503.21691"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_17"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674640"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547647"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371109"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.1804.07608"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2303.05491"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2207.04034"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523704"},{"key":"e_1_2_1_28_1","doi-asserted-by":"crossref","unstructured":"P. M\u00fcller. 2002. Modular Specification and Verification of Object-Oriented Programs (LNCS Vol. 2262). Springer.","DOI":"10.1007\/3-540-45651-1"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297027.1297061"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3443420"},{"key":"e_1_2_1_32_1","volume-title":"Patina: A Formalization of the Rust Programming Language","author":"Reed Eric W.","year":"2015","unstructured":"Eric W. Reed. 2015. Patina: A Formalization of the Rust Programming Language. University of Washington."},{"key":"e_1_2_1_33_1","volume-title":"The Polonius Reference Implementation for the Rust Borrow-Checker. https:\/\/github.com\/rust-lang\/polonius Accessed","author":"Rust","year":"2019","unstructured":"Rust contributors. 2019. The Polonius Reference Implementation for the Rust Borrow-Checker. https:\/\/github.com\/rust-lang\/polonius Accessed April 4, 2019"},{"key":"e_1_2_1_34_1","volume-title":"https:\/\/blog.rust-lang.org\/inside-rust\/2023\/10\/06\/polonius-update.html Accessed","author":"R\u00e9my Rakic and Niko Matsakis on behalf of The Polonius Working Group","year":"2025","unstructured":"R\u00e9my Rakic and Niko Matsakis on behalf of The Polonius Working Group. 2023. Polonius Update. https:\/\/blog.rust-lang.org\/inside-rust\/2023\/10\/06\/polonius-update.html Accessed March 24, 2025"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2543920"},{"key":"e_1_2_1_36_1","volume-title":"https:\/\/rust-analyzer.github.io\/ Accessed","author":"Systems Ferrous","year":"2025","unstructured":"Ferrous Systems and contributors. 2025. Rust-analyzer. https:\/\/rust-analyzer.github.io\/ Accessed July 30, 2025"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-SEIP55303.2022.9794041"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3735592"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.1804.10806"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.1806.02693"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.1903.00982"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763122","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:49:24Z","timestamp":1760032164000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763122"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":41,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763122"],"URL":"https:\/\/doi.org\/10.1145\/3763122","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-25","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}