*********************************************************************
*                       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 5 mars 2004 *** 14h00 **********************************

Jean-Christophe FILLIA^TRE (LRI, Orsay)

Why : un outil de vérification générique  

Re'sum'e:

  Nous présentons l'outil de  vérification Why. À l'instar de nombreux          
  systèmes existants,  cet outil produit  des obligations de  preuve à          
  partir de programmes annotés. Il y a cependant plusieurs différences          
  notables. D'une part, le langage  d'entrée se veut générique : c'est          
  un mini-ML  avec traits impératifs  et exceptions vers lequel  on va          
  compiler des langages existants  --- dit autrement, c'est un langage          
  intermédiaire  spécifique à la  génération d'obligations  de preuve.          
  D'autre part, les obligations  de preuve peuvent être produites pour          
  plusieurs systèmes de preuve existants : quatre assistants de preuve          
  (semi-)interactifs (Coq, PVS, HOL Light et Mizar) et deux procédures          
  de décision  (Simplify et haRVey).  Enfin, la technologie  interne à          
  l'outil  Why s'appuie  sur une  traduction fonctionnelle  à  base de          
  monades, et non  sur les règles de logique  de Hoare traditionnelles          
  (même si le résultat est souvent identique).                                  
                                                                                
  Nous détaillerons l'application pratique de cet outil à la preuve de          
  programmes Java  annotés avec JML  (Java Modeling Language) et  à la          
  preuve de programmes C.                                                       

Vendredi 12 mars 2004 *** 14h00 *********************************

Andrey RYBALCHENKO (MPI, Sarrbruecken)

Transition Invariants

Re'sume': Proof rules for the temporal verification of concurrent programs 
rely on auxiliary assertions.  We propose a (sound and relatively 
complete) proof rule whose auxiliary assertions are \emph{transition 
invariants}. A transition invariant of a program is a binary
relation over program states that contains the transitive closure o
the transition relation of the program. A transition invariant is
\emph{disjunctively well-founded} if it is a finite union of                    
well-founded relations.  We characterize the validity of a liveness             
property by the existence of a disjunctively well-founded transition            
invariant. 

Joint work with Andreas PODELSKI (MPI, Sarrbruecken)

*** Vendredi 19 mars 2004 *** 14h00 *********************************

Sarah THOMPSON (Computer Laboratory, University of Cambridge)

Abstract Interpretation of Asynchronous Circuits

Re'sume' : We present an abstract interpretation framework that allows dynamic 
properties  of asynchronous digital circuits to be statically determined. In 
our model, time is linear, dense and continuous, with the structure (but not
the arithmetic) of the real numbers. Within a finite time window, signals can be
represented by their start and end states, along with the count of complete     
cycles during the window. Defining the familiar logical operators in terms of   
these values results in a 'logic' that, given known inputs, can place bounds    
on the number and kind of transitions that may occur at the output of a         
combinational circuit. A hierarchy of simplified logics, related by Galois      
connections, have been identified that offer varying degrees of accuracy.       
Applications include simulation, model checking, synthesis and optimisation.    

Reference:                                                                     
[1] S. Thompson and A. Mycroft, Sliding Window Logic Synthesis, UK              
Asynchronous Forum, Cambridge, January 2004, Available from                     
http://st326.st-edmunds.cam.ac.uk/mypapers/                                     

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