*********************************************************************
*                       Ecole Normale Supe'rieure                   *
*                                                                   *
*                              Se'minaire                           *
*                SEMANTIQUE ET INTERPRETATION ABSTRAITE             *
*                              P. Cousot                            *
*                                                                   *
*                        Vendredi, 14h00--15h30                     *
*                 Salle W, 4e`me e'tage, toits du DMI               *
*                 DMI  ENS  45 rue d'Ulm  75005 Paris               *
*********************************************************************

*** Vendredi 7 mars 1997 **** 14h00 *********************************

Une methode de tableaux pour la logique du temps lineaire (2eme
partie)

Jean GOUBAULT (Dyade)

Re'sume' :  Apres avoir traite des operateurs Box et Diamond dans la
premiere partie (voir le resume du seminaire du Vendredi 28 fe'vrier 
1997), on traite dans la deuxieme partie le cas plus complexe des 
operateuurs Next, Until et Wait.

*** Vendredi 14 mars 1997 **** 14h00 ********************************

Implementing a Static Analyzer of Concurrent Programs: Problems and
Perspectives

Re'gis CRILIG (LIENS)

Re'sume' : In this talk we will share the design problems we experienced 
when we were implementing  a prototype analyzer of an asynchronous concurrent
language. This new kind of static analyzer is based on previous work about
operational semantics of parallel languages that can express
concurrency and non-determinism of actions: it constructs abstract automata
reflecting all the possible execution behaviours of programs written in
languages such as Parallel~Pascal or Concurrent~ML.

We will also present some experimental results dealing with the size of the 
generated automata and the precision of the analysis.
For instance some well-known mutual exclusion protocols have been automatically
proven correct.
    The analyzer has been interfaced using the HTML markup language: this 
allows the user to ask for computed invariants at given program points.

*** Vendredi 21 mars 1997 **** 14h00 ********************************

Rela^che.

*** Vendredi 28 mars 1997 **** 14h00 ********************************

Rela^che.

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