Seminar details


Room 206 (2nd floor, badged access)

26 January 2023 - 14h00
Aeneas: Rust Verification by Functional Translation
by Son Ho from 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.





Contact | Site Map | Site powered by SPIP 3.2.17 + AHUNTSIC [CC License]

info visites 1996380