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

                             Guillaume Bertholon
                               Inria Strasbourg

                   A practical Separation Logic typechecker

In this talk, I will present my work on the implementation of a
practical Separation Logic typechecker.

This typechecker takes a program written in an imperative lambda
calculus, annotated with function contracts, loop invariants, and
ghost code for shifting the view on resources.

The typechecker verifies the validity of contracts and decorates the
program AST with: (1) the resources available at every program point,
(2) for every subterm, the set of resources it uses/consumes/produces.

Exploiting this information, one can tell if two instructions commute,
if a memory cell is not modified on a scope, if a write is never read,
if a loop is parallelizable, etc.

In the OptiTrust project, we use this information to justify the
correctness of source-to-source optimizations.

I will first describe the specification language, which includes
implicit fractions for read-only permissions, uninitialized
permissions, and loop contracts featuring both invariants and
consumes/produces clauses.

I will then present several interesting aspects of the typing
algorithm, including techniques for contract minimization, for
checking that the evaluation order of function argument is irrelevant,
and for semi-automatic management of read-only permissions.

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

             Nos séminaires sont accessibles en ligne en direct
                            via le lien ci-dessus.