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

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

			     S É M I N A I R E

                   ______                __    _
                  / ____/___ _____ ___  / /_  (_)_  ______ ___
                 / /   / __ `/ __ `__ \/ __ \/ / / / / __ `__ \
                / /___/ /_/ / / / / / / /_/ / / /_/ / / / / / /
                \____/\__,_/_/ /_/ /_/_.___/_/\__,_/_/ /_/ /_/

			     I N R I A - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                          Salle Lions 1, bâtiment C

                           Lundi 23 novembre, 10h30

                                 ------------
                                 Xavier Denis
                                 ------------

Université Paris-Saclay, CNRS, Inria, Laboratoire de recherche en informatique

        ==============================================================
        Verification of Rust programs through prophecies and ownership
        ==============================================================


Deductive program verification seeks to eliminate bugs in software by
translating programs annotated with specifications into logical formulas which
are then solved using semi-automated tools.  When verifying programs using a
mutable heap, it is often required to show that pointers do not alias each
other, ensuring there is only one way to modify structures in memory.  This
leads to cumbersome proof obligations and makes verification much more
challenging.  Newer languages like Rust feature pointers as well but prevent
aliasing through the type system.  This opens the door to simpler approaches
to verification, free of tedious proof obligations.

We propose a technique for the verification of Rust programs by translation to
a functional language.  The challenge of this translation is the handling of
mutable borrows, pointers with control of aliasing in a region of memory.  To
overcome this, we used a technique inspired by prophecy variables to predict
the final values of borrows.  The main contribution of this work is to prove
this translation correct.  We developed a proof-of-concept tool to show the
viability of this approach.