Modular Specification and Verification of Closures in Rust
summary
Presents a concrete method to specify and verify Rust closures by encoding higher‑order concerns into a first-order encoding that SMT solvers (via Viper and Z3) can discharge. Adds historian invariants for relating current and past states, call descriptions for effects and call results, and behavioral-subtyping style specification entailments. Ships as an extension of Prusti, verifies many common closure idioms and iterator patterns (map, filter, fold), and reports automated verification across examples and crates from the Rust ecosystem.
AI-written summary · about
chapters (9)
- 0:00Closure verification challenges
- 1:48Rust’s type system for closures
- 2:50Prusti verifier for Rust
- 3:54Monotonicity proof with historian variants
- 6:46Higher-order functions and contracts
- 10:41Side effects in closures
- 12:53Evaluation and implementation
- 14:19Contributions and future work
- 15:52Q&A on interior mutability
related talks
15mModular Specification and Verification of Closures in Rust
25mCompositional Reasoning about Advanced Iterator Patterns in Rust
19mA Hybrid Approach to Semi-automated Rust Verification
17mRefinedRust: A Type System for High-Assurance Verification of Rust Programs
19mRavencheck: Effectively-Propositional Reasoning for Rust
20mVerusBelt: A Semantic Foundation for Verus’s Proof-Oriented Extensions to the Rust Type(…)
14mA Refinement Methodology for Distributed Programs in Rust
21mA Tour of Empirical Verification in Rust