Modular specification and verification of closures in Rust
| Autor: | Fabian Wolff, Aurel Bílý, Alexander J. Summers, Peter Müller, Christoph Matheja |
|---|---|
| Rok vydání: | 2021 |
| Předmět: |
Computer science
Programming language business.industry Rust Closures High-order functions Software verification Extension (predicate logic) computer.software_genre Automation TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Closure (computer programming) TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Code (cryptography) State (computer science) Safety Risk Reliability and Quality business computer Formal verification Software Rust (programming language) computer.programming_language |
| Zdroj: | Proceedings of the ACM on Programming Languages, 5 (OOPSLA) |
| ISSN: | 2475-1421 |
| DOI: | 10.1145/3485522 |
| Popis: | 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. Proceedings of the ACM on Programming Languages, 5 (OOPSLA) ISSN:2475-1421 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|