Modular Specification and Verification of Closures in Rust
summary
A Prusti extension encodes higher-order Rust closures into first-order Viper logic and discharges verification conditions to Z3, claiming modular verification of closure usage. It introduces history invariants to capture monotonic state across arbitrary calls, specification entailments for behavioural subtyping of passed closures, and call descriptions to name call results. The prototype verifies all Option higher-order functions and several Vec methods, runs in seconds, and catches injected errors quickly.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 0:23Closures in JavaScript
- 3:46Concrete Syntax
- 4:25Closure Verification
- 6:51Summary
- 10:19Call descriptions
- 11:38Summarize
- 12:03Implementation
- 13:00Evaluation
- 13:55Conclusion
related talks
20mModular Specification and Verification of Closures in Rust
20mVerusBelt: A Semantic Foundation for Verus’s Proof-Oriented Extensions to the Rust Type(…)
17mRefinedRust: A Type System for High-Assurance Verification of Rust Programs
19mA Hybrid Approach to Semi-automated Rust Verification
19mRavencheck: Effectively-Propositional Reasoning for Rust
25mCompositional Reasoning about Advanced Iterator Patterns in Rust
14mA Refinement Methodology for Distributed Programs in Rust
18mVerus: Verifying Rust Programs using Linear Ghost Types