*******************************************************************
*                   LIENS Ecole Normale Superieure                *
*                                                                 *
*                          Groupe de travail                      *
*              'Semantique et Interpretation Abstraite'           *
*                             P. Cousot                           *
*                                                                 *
*                        Vendredi, 10h--12h                       *
*                    Jean-Louis Verdier, passage vert             *
*                 ou  Salle Henri Cartan B, etage -2              *
*                   DMI ENS 45 rue d'Ulm 75005 Paris              *
*******************************************************************

*** Vendredi 12 mars 1993 *** Seminaire *** Jean-Louis Verdier ***

Interpre'tation abstraite et ve'rification de syste`mes communicants.

Jean-Claude Fernandez (IMAG/LGI, Grenoble)

Resume: Selon le formalisme utilise' pour repre'senter les spe'ci-
fications, on distingue deux me'thodes de ve'rification. Dans le 
cas de spe'cifications logiques (qui caracte'risent les proprie'-
te's globales du syste`me) la me'thode de ve'rification est fonde'e
sur une relation de satisfaction de'finie entre les formules et le 
mode`le. Dans le cas les spe'cifications comportementales (qui 
consistent a` de'crire le comportement attendu du programme, 
observe' a` un certain niveau d'abstraction) la me'thode de 
ve'rification est fonde'e sur une relation d'e'quivalence entre 
syste`mes de transition.
   Le proble`me pratique auxquelles sont confronte'es ces me'thodes 
est l'explosion des e'tats due au paralle'lisme.  Pour re'soudre ce 
proble`me, nous nous inte'ressons a` des formes interme'diaires plus 
e'labore'es que les syste`mes de transition classiques. Nous avons 
dans un premier temps utilise' les BDDs pour mode'liser un re'seau 
de syste`mes de transition. Nous nous inte'ressons actuellement a` 
l'utilisation de l'interpre'tation abstraite pour abstraire 
l'ensemble des e'tats dans des the'ories de'cidables (les interval-
les, les polye`dres).
   Nous illustrons cette proble'matique sur un algorithme ge'ne'rant 
un syste`me de transition minimum relativement a` une relation 
d'e'quivalence.

*** Vendredi 19 mars 1993 ****** Reunion de travail *** SALLE W ***

Domaines

Bruno Monsuez & Eric Goubault (LIENS)

*** Vendredi 26 mars 1993 *** Seminaire *** SALLE Henri Cartan B ***

Le langage Alpha et son utilisation pour la synthe`se d'architectures
systoliques.

Patrice Quinton (IRISA)

Resume: dans des domaines comme le traitement du signal, ou` des 
applications doivent e^tre re'alise'es a`  l'aide d'architectures VLSI 
paralle`les, la synthe`se d'architecture a` partir de spe'cifications 
fonctionnelles est d'une grande importance. On pre'sente un langage, 
appelle' Alpha, et son utilisation pour la synthe`se d'architectures 
systoliques -- architectures paralle`les re'gulie`res. Fonde' sur 
l'expression d'algorithmes avec des e'quations re'currentes affines, 
Alpha est un langage fonctionnel permettant la description d'algorithmes 
re'guliers, et la de'rivation formelle d'architectures synchrones
pour l'exe'cution de ces algorithmes. On de'crira les principales 
techniques de transformation permettant la synthe`se d'architectures 
systoliques, ainsi que les re'sultats que permettent d'obtenir le 
programme de synthe`se Alpha du iCentaur pour la conception de circuits. 

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