To: seminaire@pauillac.inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Moscova - 06/02/06 - Paris - FR

           Vous pouvez vous abonner à nos annonces de séminaires
             http://pauillac.inria.fr/seminaires/subscribe.html

                             S E M I N A I R E
       ___      .                       
      /    ___   __  /_  _   /             /| /|  _   __ __ _       _ 
     /    /   / /_  /   __| /    -----    / |/ | / \ /_ /  / \ | / __|
    |___ /   / __/ |_  |_/ |_            /     | |_/__/ |_ |_/ |/ |_/
                                                
                          I N R I A - Rocquencourt
                     Salle de conférences du bâtiment 8

                           Lundi 6 fevrier, 10h30

                               -------------
                               Peter O'Hearn
                               -------------

                      Queen Mary, University of London

      ================================================================
      Smallfoot:  Modular Automatic Verification with Separation Logic
      ================================================================


Separation logic is a program logic geared toward specifying and verifying
properties of dynamically-allocated linked data structures.  It has a strong
form of modularity built in, stemming from an interplay between a ``tight''
form of specification (which concentrates on program footprints) and a
connective (the separating conjunction) that allows statements about separate
portions of memory to be composed. Many by-hand proofs have been given that
illustrate this modular aspect; this work is an attempt to transfer the
modularity to an automatic setting, for (at least) a restricted class of
assertions.

This talk describes joint work with Josh Berdine and Cristiano Calcagno on
Smallfoot, an experimental tool for checking certain separation logic
specifications. It uses lightweight assertions that describe the shapes of
data structures rather than their detailed contents; this restriction allows
the reasoning to be fully automatic. Beyond the basic primitives of separation
logic Smallfoot at this point includes several hardwired shape predicates for
singly- and doubly-linked lists, for xor-linked lists, and for trees.  Hoare
triples are (soundly) decided using a form of symbolic execution of pointer
programs, together with a terminating proof theory for deciding entailments
between assertions. In the talk I will describe the basics behind Smallfoot
and give a number of examples illustrating: avoidance of frame axioms (saying
what does not change); treatment of ``dirty'' features such as memory disposal
and address arithmetic; information hiding in the presence of pointers; and
concurrency.