*********************************************************************
*                       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 6 janvier 1995 *****************************************

Abstract Interpretation of Prolog with Cut and Application to Cardinality
Analysis. (Joint work with Sabina Rossi and Pascal Van Hentenryck.)

Baudouin LE CHARLIER (F.U.N.D.P., Namur)

Re'sume' : 

Part 1: An Abstract Interpretation Framework which Accurately Handles
         Prolog Search-Rule and the Cut

A novel abstract interpretation framework is introduced, which
captures Prolog depth-first strategy and the cut operation. The
framework is based on a new conceptual idea, the notion of
substitution sequences, and the traditional fixpoint approach to
abstract interpretation. It broadens the class of analyses that are
amenable in practice to abstract interpretation and refines the
precision of existing analyses. Its practicability is demonstrated in
the second part. This part focuses on theoretical foundations.

Part 2: Cardinality Analysis of Prolog

This part instantiates the new framework to obtain a novel analysis,
called cardinality analysis, to approximate the number of solutions to 
a goal. The abstract domain captures not only modes and types but also
lower and upper bounds on the number of solutions and information about
arithmetic and meta predicates, the cut, and termination. Experimental 
results show that the approach has a number of desirable properties wrt 
efficiency, accuracy, and simplicity not available in previous work. In 
particular, all aspects of the analysis are captured in a single framework, 
the mode/type analysis and the cardinality analysis are performed 
simultaneously and termination, and abstractions of arithmetic and 
meta-predicates are used to achieve great precision, and the overhead 
of the approach is small compared to traditional mode/type analyses.


*** Vendredi 13 janvier 1995 ****************************************

M\'ethodes g\'eom\'etriques pour l'\'etude des propri\'et\'es
d'ordonnancement

\'Eric GOUBAULT (LIENS)

Re'sume' :

On parlera dans ce s\'eminaire de quelques propri\'et\'es d'ordonnancement
utiles en informatique. Parmi celles-ci,
- les propri\'et\'es de s\'equentialisation, crit\`eres de correction
pour les bases de donn\'ees parall\`eles, ou pour certaines applications
dans des languages parall\`eles \`a m\'emoire partag\'ee,
- les propri\'et\'es d'existence de protocoles pour des syst\`emes
distribu\'es, connaissant certaines contraintes,
- l'existence (et la construction!) d'ordonnanceurs pour des languages
parall\`eles sur des machines contraintes (en nombre de processeurs, en
ressources diverses et vari\'ees eventuellement en exclusion mutuelle...

Dans un premier temps, on exposera les r\'ecents travaux de J.Gunawardena
(bases de donn\'ees), M. Herlihy, N. Shavit, M. Saks, H. Attiya...
(protocoles de syst\`emes distribu\'es). Dans un deuxi\`eme temps, on
introduira une autre approche, bas\'ee sur le mod\`ele du vrai 
parall\'elisme des automates de dimension sup\'erieure.
On d\'eveloppera une th\'eorie de l'homotopie permettant de d\'efinir
la notion d'ordonnanceur d'un programme sur n processeurs (n entier
quelconque). On montrera que d\'eriver ces ordonnanceurs peut se faire
par interpr\'etation abstraite et on donnera quelques id\'ees d'algorithmes
pour ce faire.


*** Vendredi 20 janvier 1995 ****************************************

Rela^che

*** Vendredi 27 janvier 1995 ****************************************

Rela^che

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