Open access
Date
2021-10Type
- Conference Paper
Abstract
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.
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. Show more
Permanent link
https://doi.org/10.3929/ethz-b-000512454Publication status
publishedExternal links
Journal / series
Proceedings of the ACM on Programming LanguagesVolume
Pages / Article No.
Publisher
Association for Computing MachineryEvent
Subject
Rust; Closures; High-order functions; Software verificationOrganisational unit
03653 - Müller, Peter / Müller, Peter
More
Show all metadata