Séminaire Cambium, Inria Paris, 2 rue Simone Iff
                            Salle A215, bâtiment A
                             Lundi 16 mai, 10h30

                                    Son Ho
                                 Inria Paris

             Aeneas: Rust Verification by Functional Translation

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.

            Vous pouvez vous abonner à nos annonces de séminaires:
                     http://cambium.inria.fr/seminar.html

             Nos séminaires sont accessibles en ligne en direct:
                  https://webconf.math.cnrs.fr/b/fra-ryy-fjn