*********************************************************************
*                       Ecole Normale Supe'rieure                   *
*                                                                   *
*                              Se'minaire                           *
*                SEMANTIQUE ET INTERPRETATION ABSTRAITE             *
*                              P. Cousot                            *
*                                                                   *
*                        Vendredi, 14h00--15h30                     *
*                           Salle U/V, etage -2                     *
*                  DI  ENS  45 rue d'Ulm  75005 Paris               *
*********************************************************************

*** Vendredi 25 octobre 2002 **** 14h00 ******************************
             ^^^^^^^^^^^^^^^

John C. Reynolds (Carnegie Mellon University & Queen Mary, University
                  of London)

A Logic for Shared Mutable Data Structures

Re'sume' :
In joint work with Peter O'Hearn and others, based on early
ideas of Burstall, we have developed an extension of Hoare logic
that permits reasoning about low-level imperative programs that
use shared mutable data structure.

The simple imperative programming language is extended with commands
(not expressions) for accessing and modifying shared structures, and
for explicit allocation and deallocation of storage.  Assertions are
extended by introducing a ``separating conjunction'' that asserts that
its subformulas hold for disjoint parts of the heap, and a closely
related ``separating implication''.  Coupled with the inductive
definition of predicates on abstract data structures, this extension
permits the concise and flexible description of structures with
controlled sharing.

In this talk, we will survey the current development of this program
logic, including extensions that permit unrestricted address arithmetic,
dynamically allocated arrays, and recursive procedures.  We will also
discuss promising future directions.

*********************************************************************
Pour recevoir l'annonce par courrier electronique: cousot@di.ens.fr
WWW: http://www.di.ens.fr/~cousot/annonceseminaire.html
*********************************************************************