{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:43:03Z","timestamp":1767926583565,"version":"3.49.0"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T00:00:00Z","timestamp":1634256000000},"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":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2021,10,20]]},"abstract":"<jats:p>Closures are a language feature supported by many mainstream languages, combining the ability to package up references to code blocks with the possibility of capturing state from the environment of the closure's declaration. Closures are powerful, but complicate understanding and formal reasoning, especially when closure invocations may mutate objects reachable from the captured state or from closure arguments.<\/jats:p>\n          <jats:p>This paper presents a novel technique for the modular specification and verification of closure-manipulating code in Rust. Our technique combines Rust's type system guarantees and novel specification features to enable formal verification of rich functional properties. It encodes higher-order concerns into a first-order logic, which enables automation via SMT solvers. Our technique is implemented as an extension of the deductive verifier Prusti, with which we have successfully verified many common idioms of closure usage.<\/jats:p>","DOI":"10.1145\/3485522","type":"journal-article","created":{"date-parts":[[2021,10,15]],"date-time":"2021-10-15T19:18:28Z","timestamp":1634325508000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":22,"title":["Modular specification and verification of closures in Rust"],"prefix":"10.1145","volume":"5","author":[{"given":"Fabian","family":"Wolff","sequence":"first","affiliation":[{"name":"ETH Zurich, Switzerland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9284-9161","authenticated-orcid":false,"given":"Aurel","family":"B\u00edl\u00fd","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9151-0441","authenticated-orcid":false,"given":"Christoph","family":"Matheja","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}]},{"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-5554-9381","authenticated-orcid":false,"given":"Alexander J.","family":"Summers","sequence":"additional","affiliation":[{"name":"University of British Columbia, Canada"}]}],"member":"320","published-online":{"date-parts":[[2021,10,15]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428204"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360573"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411235"},{"key":"e_1_2_2_5_1","unstructured":"Ernie Cohen Mark A. Hillebrand Stephan Tobies Micha\u0142 Moskal and Wolfram Schulte. 2015. Verifying C Programs: A VCC Tutorial. https:\/\/bit.ly\/32BkCWN Working draft version 0.2.  Ernie Cohen Mark A. Hillebrand Stephan Tobies Micha\u0142 Moskal and Wolfram Schulte. 2015. Verifying C Programs: A VCC Tutorial. https:\/\/bit.ly\/32BkCWN Working draft version 0.2."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71289-3_26"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.1996.493421"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380413"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581484"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-0456-4_2"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.5"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596627.1596634"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_19"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.3929\/ETHZ-A-006843251"},{"key":"e_1_2_2_17_1","unstructured":"Steve Klabnik and Carol Nichols. 2021. The Rust Programming Language. https:\/\/doc.rust-lang.org\/book\/  Steve Klabnik and Carol Nichols. 2021. The Rust Programming Language. https:\/\/doc.rust-lang.org\/book\/"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/6.4.308"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2766446"},{"key":"e_1_2_2_21_1","unstructured":"Gary T Leavens Erik Poll Curtis Clifton Yoonsik Cheon Clyde Ruby David Cok Peter M\u00fcller Joseph Kiniry Patrice Chalin and Daniel M Zimmerman. 2008. JML reference manual.  Gary T Leavens Erik Poll Curtis Clifton Yoonsik Cheon Clyde Ruby David Cok Peter M\u00fcller Joseph Kiniry Patrice Chalin and Daniel M Zimmerman. 2008. JML reference manual."},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/197320.197383"},{"key":"e_1_2_2_24_1","unstructured":"Nicholas D. Matsakis. 2013. The Case of the Recurring Closure. http:\/\/smallcultfollowing.com\/babysteps\/blog\/2013\/04\/30\/the-case-of-the-recurring-closure  Nicholas D. Matsakis. 2013. The Case of the Recurring Closure. http:\/\/smallcultfollowing.com\/babysteps\/blog\/2013\/04\/30\/the-case-of-the-recurring-closure"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2692956.2663188"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133909"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006953"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411237"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13953-6_5"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_1"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/331605.331611"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70594-9_17"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297027.1297053"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13464-7_14"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2160910.2160911"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39993-3_15"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_9"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2499370.2491978"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.3929\/ethz-b-000444764"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.5482557"},{"key":"e_1_2_2_43_1","volume-title":"Summers","author":"Wolff Fabian","year":"2021"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71389-0_26"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485522","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3485522","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:40Z","timestamp":1750191520000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3485522"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,15]]},"references-count":42,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2021,10,20]]}},"alternative-id":["10.1145\/3485522"],"URL":"https:\/\/doi.org\/10.1145\/3485522","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,10,15]]},"assertion":[{"value":"2021-10-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}