*********************************************************************
*                       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 19 Septembre **** 14h00 ********************************

Eben UPTON (Cambridge U., visiteur du STIX)

Static Analysis of Gated Data Dependence Graphs

Re'sume':
Several authors have advocated the use of the gated data dependence graph
as a compiler intermediate representation. In this paper we describe the
design of a static analysis for this representation, using the methodology
of abstract interpretation. A concrete semantics is presented, and the
soundness of the analysis with respect to this semantics is shown. The
analysis is parameterized by the underlying numerical domain.

*** Vendredi 26 Septembre **** 15h00 ********************************

Pavol CERNY (ENS)

Verification by abstract intepretation of parametrized predicates

Re'sume': Predicate abstraction is a well-known and widely used
abstract interpretation technique for verification of programs
and systems. The user specifies the abstract domain by choosing
a set of predicates on values and variables of the program.
Thus one of the shortcomings of this method is that the user
intervention is program-specific and therefore has to be repeated
for different programs even if they are very similar.
In this work, we present a generalization, predicate abstraction
with parametrized predicates. It allows the user to specify
the predicates with respect to the problem (e.g. sorting by comparison)
or the programming language. The abstract generic predicate domain
is constructed using a relational abstract domain.
In our implementation, we used the octagon abstract domain both as the
relational domain and as a decision procedure.

We demonstrate our methods on several simple examples, such as array
initialization and sorting algorithms and we discuss several possible 
extensions.

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