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

*** Vendredi 29 avril 1994 ***************************************

Abstraction in Truly Concurrent Bisimulation

Sophie Pinchinat (LIFIA, IMAG, Grenoble ; University of Sussex -
                  Brighton)

Re'sume' : During the last decade, partial order semantics have been 
studied in depth as a promising approach to the semantic aspects of 
reactive systems. Such semantics enable one to formalise interesting 
features of the systems and most importantly, they no longer identify
concurrency and sequential non-determinism as it is in interleaving
models.

In particular, partial order semantic equivalences may be used to
define notions of systems' behaviour in a way which is independent of
the level of atomicity of the actions performed by the system.

Formally, provided an operation over systems - known as the refinement
of actions - which replaces actions by (more) complexe subsystems, one
is interested in defining compositional semantics, ie semantic
congruences w.r.t. this operation.

In the concret models setting (ie models where any action is

In this talk, we show how to combine partial order semantics with
interleaving ones to provide us with a mechanism to hide actions that
are not observable.

(joint work with Rob van Glabbeek, Stanford)

*** Vendredi 6 mai 1994 *********************************************

Systemes de transitions de dimension superieure:

Eric GOUBAULT (LIENS)

Re'sume' : On introduit ici la notion de systemes de transitions de 
dimension superieure (basee sur des idees de Vaughan Pratt et de Rob 
van Glabbeek). Ces systemes de transitions permettent de donner des
semantiques operationnelles  du ''vrai parallelisme''. La formulation
algebrique agreable qui en resulte donne egalement une theorie
denotationnelle interessante.

Une variante utilisant des idees d'algebre homologique (les automates
de dimension superieure) permet d'etudier la ''geometrie'' du systeme
de transitions: test d'equivalence semantique ''branching-time'' 
(bisimulation, failure pairs...), sequentialisation, deadlocks,
branchements, confluences...D'autres variantes seront presentees comme
celle permettant de donner des semantiques du temps reel.

On donnera ensuite un apercu des rapports entre systemes de transitions
de dimension superieure et d'autres modeles operationnels du vrai
parallelisme (systemes de transitions asynchrones, systemes de transitions
avec independance, traces de Mazurkiewitz...) en comparant en particulier
leur pouvoir expressif (en terme de proprietes d'exclusion mutuelle et
de niveau de parallelisme).

Enfin, on montrera comment construire des systemes de preuves ou des
interpretations abstraites de languages paralleles a partir de leurs
semantiques decrites par des systemes de transitions de dimension 
superieure.

*** Vendredi 13 mai 1994 ********************************************

Relache

*** Vendredi 20 mai 1994 ********************************************

Relache

*** Vendredi 27 mai 1994 ********************************************

Interpretation abstraite en programmation logique avec contraintes

Christophe LECOUTRE (LIFL, Lille)

Re'sume' : Nous proposons un modele generique d'interpretation abstraite 
applique a la programmation logique avec contraintes. Ce modele est compose
d'une phase d'extension du domaine suivie d'une phase d'abstraction du 
calcul. L'extension du domaine consiste a integrer de nouvelles contraintes 
au domaine d'un CLP-langage et l'abstraction du calcul consiste a forcer 
la terminaison de la resolution OLD via l'utilisation conjuguee d'une 
technique de tabulation et d'operateurs d'elargissement (widening).

Nous illustrons ce modele avec une application non triviale portant sur
l'inference de types en Prolog. Pour cette analyse, l'extension du domaine 
correspond a l'integration de contraintes ensemblistes. Ainsi, les 
contraintes du langage obtenu portent a la fois sur les termes (ou arbres) 
finis et sur les ensembles. L'interet de cette combinaison est que les 
contraintes sur les termes permettent de coder les dependances entre les 
variables et que les contraintes ensemblistes permettent de coder les 
structures recursives et non deterministes.

*********************************************************************