Détails sur le séminaire

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.

Contact | Plan du site | Site réalisé avec SPIP 3.2.17 + AHUNTSIC [CC License]

info visites 1996392