Rust Verification by Functional Translation
24/03/2023, 3pm
Speaker
Abstract
We present Aeneas, a new verification toolchain for Rust programs based on a lightweight functional translation. We leverage Rust's rich region-based type system to eliminate memory reasoning for a large class of Rust programs by translating them to a pure lambda-calculus, as long as they do not rely on interior mutability or unsafe code. Doing so, we relieve the proof engineer of the burden of memory-based reasoning, allowing them to instead focus on functional properties of their code.
Bio
Son Ho is a Ph.D. candidate working at INRIA in the Prosecco team, under the supervision of Karthikeyan Barghavan and Jonathan Protzenko. His research field is the formal verification of computer programs.