Orateur: Aymeric Fromherz (Inria)
Quand: le mercredi 30 avril 2025 de 16 h à 17 h
Où: PK-5115, Pavillon Président-Kennedy (UQAM), 201 avenue du Président-Kennedy
Diapos: PDF

Résumé: The Rust programming language has recently gained traction in industrial settings and in the systems community. A large part of this success stems from several key features of the language: Rust provides both the high performance and low-level idioms commonly associated to languages like C and C++, as well as memory safety by default thanks to its rich, borrow-based type system. However, despite being safer than C or C++, Rust programs are not immune to bugs and vulnerabilties, including aborted executions (i.e., Rust’s panic), incorrect uses of the unsafe escape hatch, or simply programs that do not match their expected behaviour, raising the need for novel static analyzers and verification tools.

To this end, we present Aeneas, a new toolchain geared towards the formal verification of Rust programs. Aeneas leverages Rust’s region-based type system to eliminate memory reasoning for a large class of Rust programs: relying on a custom borrow-centric symbolic execution, the toolchain translates safe Rust programs to a semantically equivalent functional model in proof assistants such as Lean, Rocq, or F*, enabling the use of powerful logics to specify and reason about programs.

In this talk, we will show the core ideas behind Aeneas’ functional translation on several examples, and present the broader ecosystem around Aeneas, including the Charon analysis framework and ongoing work on transpilers between C and Rust to handle legacy systems.