Room 206 (2nd floor, badged access)
26 janvier 2023 - 14h00
Aeneas: Rust Verification by Functional Translation
par Son Ho de Team Prosecco of Inria Paris
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.
