*********************************************************************
*                       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 20 mai 2005 **** 14h00 *********************************

George Necula (University of Berkeley, visiting ENS)

Data Structure Specifications via Local Equality Axioms

Abstract : We describe a program verification methodology for specifying
global shape properties of data structures by means of axioms involving
arbitrary predicates on scalar fields and pointer equalities in the
neighborhood of a memory cell.  We show that such local invariants are both
natural and sufficient for describing a large class of data structures.  We
describe a complete decision procedure for such a class of axioms.  The
decision procedure is not only simpler and faster than in other similar
systems, but has the advantage that it can be extended easily with
reasoning for any decidable theory of scalar fields.

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