*********************************************************************
*                       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 3 mai 1996 **** 14h00 **********************************

Relache.

*** Vendredi 10 mai 1996 **** 14h00 *********************************

Groupe de travail (http://www.ens.fr/~cousot/annoncegdtravail.html)

*** Vendredi 17 mai 1996 **** 14h00 *********************************

Relache

*** Vendredi 24 mai 1996 **** 14h00 *********************************

Analyse de comportement par interpretation abstraite

Franck VE'DRINE (LIX)

Re'sume' : L'analyse de comportement est originellement definie par Patrick
& Radhia Cousot  comme une generalisation  des analyses  de necessite,  de
terminaison, de projection et de relations partielles d'equivalence. Cette
definition sera etendue  aux temps de liaisons,  au typage et aux flots de
donnees.  Dans  ce  talk,  j'essaierai  de  montrer  que  l'interpretation
abstraite est particulierement bien adaptee  pour une telle analyse.  Dans
un premier temps,  je presenterai un domaine abstrait tres precis base sur
une  theorie  des  ensembles  assez  simple  pour  un langage  fonctionnel
paresseux.   Ensuite,   je  montrerai  comment  inferer  efficacement  des
proprietes  sur  ce domaine abstrait  et  motiverai  l'introduction  d'une
deuxieme  correspondance  de Galois  validant l'analyse  et  permettant de
prouver automatiquement  certaines  proprietes  de terminaison totale  par
recurrence. De nombreux exemples devraient illustrer le talk.

*** Vendredi 31 mai 1996 **** 14h00 *********************************

Relache.

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