*********************************************************************
*                       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 4 fevrier 2000 **** 14h00 ******************************

Rela^che.

*** Vendredi 11 fevrier 2000 **** 14h00 *****************************

Vacances de fevrier / winter holidays

*** Vendredi 18 fevrier 2000 **** 14h00 *****************************

Jean-Luc Lambert (Valiosys SA)

LPV: a new technique to formally prove or disprove safety properties

Re'sume' : 

A lot of logical theories were used in order to prove that a software or a
hardware system satisfies predefined safety properties. Strangely the
linear programming theory was left beside and never considered as a theory
to make formal proof. Even so it appears that linear programming, by the
way of the duality theorem, is a logical theory with nice completeness
properties. Moreover proving with linear programming uses well-known
efficient polynomial time algorithms.

In this talk we will show how the behavior of a software/hardware system
can be modeled with linear programming and we will show that the duality
theorem gives an inference engine that is both powerful and algorithmically
efficient.

*** Vendredi 25 fevrier 2000 **** 14h00 *****************************

Rela^che.

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