*******************************************************************
*                   LIENS Ecole Normale Superieure                *
*                      Les vendredis de l'equipe                  *
*              'Semantique et Interpretation Abstraite'           *
*                              P. Cousot                          *
*             Salle J-L Verdier, Passage Vert, 14h--16h           *
*                 DMI ENS 45 rue d'Ulm 75005 Paris                *
*******************************************************************

*** Vendredi 9 octobre 1992 *** Reunion de travail ****************

B. Monsuez  Higher-order strictness analysis by type inference.

*** Vendredi 16 octobre 1992 *** Seminaire ************************

Une methode rapide de preuve automatique en logique classique du
premier ordre.

Jean Goubault (BULL)

Resume: le theoreme de Herbrand, fondement des methodes completes
de demonstration automatique actuelles comme la resolution ou la
methode des connexions, est ici soumise a un reexamen. La preuve
devient un probleme de jeux sur des graphes entre un planificateur
et un unificateur, le but du planificateur etant de reduire la
formule de depart a une tautologie, celui de l'unificateur etant
de reduire la marge de manoeuvre du precedent. Une strategie de
recherche de la preuve, fondee sur le principe de la minimisation
du facteur de branchement dans l'arbre de recherche, est presentee.
Les resultats, tant pratiques (benchmarks) que theoriques (nature
et complexite des problemes de preuve), seront degages. Les
analogies avec les methodes plus classiques seront esquissees.

*** Vendredi 23 octobre 1992 *** Seminaire ************************

Type Inference by Abstract Interpretation

Bruno Monsuez (LIENS)

Resume: We presents a generic method which uses the framework of
Abstract Interpretation as defined by the Cousots to build type
reconstruction algorithms. Fundamentally, this method is based upon
the combination of an upper and a lower approximation as well as
the use of widening operators to insure algorithm termination. We
illustrate this method with a type reconstruction algorithm of the
expressions of a ML-like language more or less similar to ML+. We
first show that restricting recursive constants to monomorphic types
-- as in ML -- can be seen as a widening operator. Then we exhibit
a less restrictive operator which lets recursive defined expressions
have polymorphic types, while still insuring algorithm termination.

*** Vendredi 30 octobre 1992 *** Relache **************************

*** Vendredi 6 novembre 1992 *** Reunion de travail ***************

Eric Goubault Des modeles du parallelisme.

*** Vendredi 12 novembre 1992, DEC PRL, 16h *** Soutenance de these 

Semantiques des langages imperatifs d'ordre superieur
et interpretation abstraite

Francois Bourdoncle (DEC-PRL)

Resume: L'interpretation abstraite ou analyse semantique d'un 
langage de programmation est une methode formelle permettant 
d'obtenir, de maniere statique (i.e. la compilation) et automatique, 
une description approchee du comportement dynamique (i.e. a 
l'execution) des programmes. Cette methode a ete appliquee, 
jusqu'ici, a des langages relativement simples (langages imperatifs, 
fonctionnels, logiques ou paralleles du premier ordre).  Or les 
langages de programmation modernes comme le langage Modula-3 ou 
meme des langages plus anciens comme Pascal comportent des 
mecanismes de programmation puissants (passage des parametres 
formels par reference, passage en parametre des procedures
locales, sauts a des labels non locaux, exceptions) qui augmentent
de maniere considerable leur puissance d'expression et leur
complexite semantique. Cette these aborde le probleme de 
l'interpretation abstraite des langages imperatifs d'ordre 
superieur. Dans une premiere partie, nous montrons que des 
interpretations abstraites trop ``naives'' de tels langages d'ordre 
superieur peuvent devenir a la fois extremement couteuses 
et imprecises. Pour remedier a ces problemes, nous introduisons 
une nouvelle semantique des langages imperatifs d'ordre superieur 
dont l'interpretation abstraite est precise et peu couteuse et
nous etablissons la correction de cette semantique pour une
classe non decidable de programmes comprenant en particulier la
classe decidable des programmes Pascal. Puis, dans la
seconde partie, nous abordons la technique du debugging abstrait
permettant d'effectuer une mise au point formelle des programmes et
nous presentons le systeme Syntox permettant d'effectuer
le debugging abstrait du langage Pascal par la determination
de l'intervalle de variation des variables scalaires des programmes.

DEC PRL 85, avenue Victor Hugo, 92563 Rueil-Malmaison

*** Vendredi 20 novembre 1992 *** Seminaire **********************

Parallelisme, automates et topologie algebrique

Eric Goubault (LIENS)

Resume : L'objet de ce seminaire est de presenter une generalisation 
des automates sequentiels classiques aux automates ``de dimension 
superieure'' qui fournissent un modele du ``vrai parallelisme'',
c'est a dire qu'ils distinguent choix non-deterministe et execution
concurrente. On montrera que la geometrie de ces automates nous 
permet de discuter de notions telles que: branchements, deadlocks, 
divergences, sequentiabilisation, mais aussi d'analyser un certain 
nombre d'equivalences semantiques comme la bisimulation, failure 
equivalence... Cette geometrie peut etre decrite purement 
algebriquement en utilisant des outils nous venant de la topologie 
algebrique. Le modele lui-meme a une expression algebrique 
directement en termes d'objets d'algebre homologique. Cela nous 
donne des methodes de calculs effectifs pour enumerer les deadlocks, 
semi-decider d'equivalences semantiques... Des exemples seront 
donnes en decrivant CCS dans notre formalisme.


*** Vendredi 27 novembre 1992 *** Reunion d'equipe ***************

Quelques idees naives sur les semantiques en style de passage a
la continuation.

Jean Goubault  (BULL)

Resume: le style de passage a la continuation (CPS) a permis dans 
le passe de donner une semantique denotationnelle de langages 
fonctionnels comme Scheme, presentant un "goto generalise" appele 
capture de continuation (call/cc). Nous montrons que le CPS 
s'etend naturellement, lorsque l'on autorise le non-determinisme 
dans le langage, a un formalisme de transformateur de predicats 
parametres, rappelant les semantiques en arriere de Hoare. 
Independamment du non-determinisme, nous presentons une autre 
idee naive d'extension pour modeliser le parallelisme. L'idee de 
base est d'introduire des echelles de temps locales aux processus; 
ces temps disparaissent ensuite du formalisme, dans la veine des 
semantiques des langages synchrones. La theorie n'est pas developpee, 
seules les idees de depart seront presentees.

*** Vendredi 4 decembre 1992 *** Relache *************************

*** Vendredi 11 decembre 1992 *** Seminaire **********************

Analyse par projections et interpretation abstraite

Regis Cridlig (LIENS)

Resume: Nous parlerons ici de l'analyse statique des programmes 
fonctionnels, et en particulier de ceux ecrits dans un langage 
paresseux. Une des analyses les plus utiles dans ce contexte est 
l'analyse de necessite, dont il existe beaucoup de sortes differentes : 
l'analyse par projections en est une, initialement developpee par 
P. Wadler et R. J. M. Hughes. Dans le cadre de la semantique 
denotationnelle, nous montrerons comment l'analyse par projections 
peut etre comprise comme une abstraction des expressions dans un 
contexte donne par une fonction des proprietes projectives de ce 
contexte vers un treillis abstrait de proprietes disjonctives. Cela 
permet de degager des regles simples d'analyse et de prouver leur 
surete pour un langage de premier ordre. L'analyse par projections 
peut etre etendue de differentes manieres pour traiter le cas des 
fonctions d'ordre superieur; la plus connue est sa generalisation 
aux relations d'equivalence partielles, decouverte par S. Hunt.
Finalement, nous presenterons une equivalence entre la methode 
classique d'analyse par ideaux et l'usage d'une certaine classe de 
projections.   


*** Vendredi 18 decembre 1992 *** Seminaire **********************

ARRAY OPERATIONS ABSTRACTION USING SEMANTIC ANALYSIS OF TRAPEZOID
CONGRUENCES

Francois Masdupuis (Ecole des Mines)

Resume : With the growing use of vector supercomputers, efficient
and accurate data structure analyses are needed. What we propose
in this talk is to use the quite general framework of Cousot's
abstract interpretation for the particular analysis of multi-
dimensional array indexes. While such indexes are integer tuples,
a relational integer analysis is first required. This analysis
results of a combination of existing ones that are interval and
congruence based. Two orthogonal problems are directly concerned
with the results of such an analysis, that are the parallelization/
vectorization with the dependence analysis and the data locality
problem used for array storage management. After introducing the
analysis algorithm, this paper describes on a complete example
how to use it in order to optimize array storage.
******************************************************************