L'équipe s'est constituée en octobre 1991 à l'occasion du recrutement comme professeur de Patrick Cousot. L'axe principal de recherche de l'équipe est l'interprétation abstraite [242, 229] dans ses aspects théoriques concernant la conception et l'approximation de sémantiques [240] et ses aspects appliqués concernant l'analyse sémantique et la vérification de programmes [230]. Au travers d'un séminaire hebdomadaire, le groupe conserve des liens privilégiés avec l'équipe <<Sémantique, preuve et interprétation abstraite>> du LIX, que Patrick Cousot a créée et dirigée jusqu'au 1er octobre 1991.
Les buts de recherche dans cette équipe sont de développer les modèles de sémantiques, les fondements de l'interprétation abstraite et l'analyse sémantique des programmes.
Si toutes les méthodes de définition de sémantiques des langages de programmation procèdent de manière compositionnelle par induction sur la syntaxe, elles diffèrent généralement dans leur style de présentation, que ce soit par point fixe, sous forme équationnelle, de contraintes, de conditions de fermeture, par un système formel à base de règles ou par un jeu. Nous avons étendu tous ces modes de présentation aux comportements infinis [266, 240], ce qui permet alors de montrer l'équivalence de ces divers modes de présentation [226]. Ces présentations de sémantiques étant conservées par interprétation abstraite [226], il devient possible de comprendre toutes les sémantiques d'un langage de programmation comme des approximations les unes des autres. Ceci permet de construire des hiérarchies de sémantiques [266, 240] qui diffèrent seulement par la précision de la description de l'exécution et le mode de présentation. Par exemple [266] une sémantique opérationnelle du parallélisme peut s'approcher par le non-déterminisme. On obtient une sémantique de traces finies ou infinies. Ignorant les états intermédiaires, on obtient une sémantique dénotationnelle. Ignorant la non-terminaison, on obtient une sémantique naturelle. Considérant des ensembles d'états, on obtient les transformateurs de prédicats. Décrivant ces ensembles par des langages formels, on obtient des sémantiques axiomatiques sur lesquelles sont basées les méthodes de preuve [240]. Il s'agit à terme de trouver un modèle de sémantique et une présentation indépendants d'un langage de programmation particulier, rôle que jouent les systèmes de transition dans le cas des sémantiques opérationnelles de petits pas.
Si les modèles mathématiques du calcul sont bien connus pour les langages séquentiels, il n'en va pas de même dans le cas du parallélisme où il faut prendre en considération l'exécution simultanée d'actions concurrentes, synchrones ou asynchrones. C'est pourquoi nous étudions les modèles opérationnels du << vrai >> parallélisme basés sur la notion d'automate de dimension supérieure issue des idées de Vaughan Pratt et Rob van Glabbeek (Stanford University). Ces modèles sont extrêmement flexibles puisqu'ils permettent de définir de façon dénotationnelle ou bien opérationnelle des langages parallèles aussi divers que Linda, Parallel Pascal (avec des variables partagées) ou Concurrent ML (communications via des messages). Par interprétation abstraite, ils permettent de construire effectivement un automate approché qui modélise les comportements dynamiques possibles du programme considéré, pour faire, par exemple, des analyses de systèmes infinis par model-checking abstrait.
Un automate de dimension supérieure est similaire aux automates classiques, dans le sens où l'on a toujours des états, et des transitions reliant les états. Pour exprimer le parallélisme, et même le vrai parallélisme (qui se distingue des traductions par entrelacements, identifiant non-déterminisme et parallélisme), on rajoute des transitions de dimension supérieure exhibant le degré d'asynchronie que l'on peut avoir dans l'exécution d'un programme. Ces transitions peuvent se représenter géométriquement, tout comme les transitions << ordinaires >> (de dimension 1, car ce sont des segments) et les états (ou transitions de dimension 0, car ce sont des points). Par exemple, l'entrelacement a.b+b.a (notation CCS) a pour représentation comme automate quatre transitions de dimension 1 formant le bord d'un carré. Remplir le carré consiste à rajouter une transition de dimension 2, et donc à indiquer l'indépendance des actions a et b. Les dimensions d'ordre supérieur décrivent donc le degré de parallélisme effectif lors de l'exécution d'opérations concurrentes. Cette information supplémentaire est importante pour effectuer certaines analyses de programmes comme l'exclusion mutuelle ou l'indépendance entre actions et valider des propriétés liées à la géométrie des systèmes de transitions (blocages, branchements, etc.).
On voit déjà dans l'exemple ci-dessus que certaines propriétés géométriques ont une signification en terme de propriétés des exécutions possibles. Ici le trou (carré vide) indique une exclusion mutuelle, alors que le carré plein dénote le vrai parallélisme. D'autres propriétés ont un caractère géométrique également comme les blocages (deadlocks), les branchements et confluences, et donc les équivalences sémantiques << branching-time >>, l'ordonnancement des actions, etc. Tout ceci peut se traiter algébriquement de façon élégante en utilisant des outils de topologie algébrique et d'algèbre homologique [275]. Le modèle lui-même des automates de dimension supérieure peut se formaliser à travers la notion de complexe double de modules (algèbre homologique). Des critères purement algébriques ont été développés pour définir et calculer les propriétés précédemment citées. Par interprétation abstraite, il en découle naturellement des algorithmes d'analyse d'ordonnancement [251]. À terme, on devrait pouvoir disposer d'un prototype d'analyseur permettant de prouver des propriétés de correction partielle concernant les accès à des objets partagés ou l'ordonnancement des synchronisations et des messages.
On peut définir diverses sortes de systèmes de transitions de dimension supérieure. Les systèmes totaux (HTS) décrivent toutes les transitions de dimension supérieure qui vérifient une propriété de confluence locale. Ils permettent de modéliser la confluence et le branchement à tout niveau de parallélisme. Les systèmes partiels (PHTS) permettent de plus de modéliser l'interférence entre plusieurs actions parallèles, comme par exemple la lecture et l'écriture par deux processeurs d'une même location mémoire.
Le caractère géométrique du modèle des automates de dimension supérieure incite à des généralisations intéressantes telles les automates décrivant les systèmes temps réel et les systèmes probabilistes. Nous avons montré comment obtenir des sémantiques opérationnelles vraiment parallèles, temps réel (éventuellement continu) [252]. Les constructions catégoriques permettent d'ailleurs de donner des lois pour le temps très raisonnables. Enfin les méthodes géométriques développées dans le cas sans temps se transportent aisément au cas avec temps.
Pour comparer les nombreux autres modèles du vrai parallélisme, nous avons développé une nouvelle sémantique opérationnelle du calcul de processus CCS enrichie avec des étiquettes permettant d'encoder l'arbre de dérivation des transitions. Cette information permet de retrouver de nombreux modèles sémantiques classiques sans entrelacement comme la causalité. Nous avons montré que l'approximation de la sémantique enrichie par la sémantique de causalité est une interprétation abstraite modélisée par une correspondance de Galois entre les deux modèles. Des définitions similaires devraient permettre de retrouver de nombreux modèles sémantiques présentés dans la littérature [281].
L'interprétation abstraite consiste à approcher des propriétés concrètes des programmes par des propriétés abstraites. Au cas où toute propriété concrète a une meilleure approximation dans le domaine de propriétés abstraites, la correspondance entre les propriétés concrètes et abstraites s'établit traditionnellement par une correspondance de Galois. Cette propriété est très puissante car la sémantique concrète et l'approximation définie par la correspondance de Galois définit entièrement la sémantique abstraite qui se déduit constructivement de la sémantique concrète sans avoir à faire de nouvelles approximations. Cette hypothèse est souvent forte quand une propriété concrète peut s'approcher par plusieurs propriétés abstraites sans pour autant qu'il y en ait une plus précise que les autres. Pour prendre un exemple simple, c'est le cas quand il s'agit de décrire un langage sous contexte par une grammaire algébrique. Nous avons étudié les correspondances possibles dans ce cas qu'elles soient basées sur une relation d'approximation, une fonction de concrétisation, une fonction d'abstraction, étudié les situations duales et leurs cas particuliers où interviennent les correspondances de Galois. Ceci conduit à définir des notions de complétude relatives à divers degrés d'abstraction [237].
Quand les propriétés d'un programme sont exprimées comme solutions d'un système d'équations sur un domaine sémantique infini, l'utilisation d'une correspondance de Galois et d'équations abstraites formalise l'idée de simplification des équations par approximations discrètes. Une autre façon traditionnelle de procéder pour résoudre les équations consiste à utiliser un élargissement/ rétrécissement (widening/narrowing) ce qui formalise l'idée de résolution itérative avec accélération de la convergence par extrapolation. Cette seconde méthode est souvent méconnue ou mal employée (par exemple en utilisant un domaine fini pour effectuer les élargissements). Nous avons montré qu'elle est plus puissante que l'utilisation d'une correspondance de Galois dans un domaine satisfaisant garantissant la terminaison des itérés (satisfaisant par exemple la condition de chaîne). Plus précisément une telle correspondance peut être trouvée pour chaque programme mais il n'en existe en général aucune permettant de trouver pour tous les programmes d'un langage de programmation les mêmes résultats d'analyse de programmes que ceux obtenus en utilisant les techniques élargissement/ rétrécissement dans un domaine abstrait infini. Ceci a été utilisé pour résoudre des problèmes de convergence laissés ouverts ou résolus grossièrement [243].
Comme évoqué précédemment, les techniques d'analyse
sémantique de programmes ont été principalement présentées
sous forme de points fixes ou équationnelles. Depuis peu, la
présentation sous forme de règles est plus courante. Nous avons
introduit G 
SOS, une généralisation de SOS pour
décrire des comportements infinis [267] et montré que
les présentations sous forme de point fixe, équationnelle, de
contraintes, de conditions de fermeture, par un système formel à
base de règles ou par un jeu sont équivalentes et conservées par
approximation basée sur une correspondance de Galois
[226].
L'étude d'un domaine abstrait consiste à imaginer un modèle mathématique de propriétés de programmes. Pour être utilisable pour l'analyse automatique de programmes, il faut en concevoir une représentation machine efficace et trouver des algorithmes performants donnant une version abstraite des opérations/fonctions élémentaires que l'on trouve dans la plupart des langages de programmation.
Il s'agit d'utiliser une représentation symbolique des fonctions booléennes pour construire des interprétations abstraites plus performantes quand les propriétés abstraites sont exprimées sous forme de propositions logiques. Les représentations utilisées sont les TDGs (Typed Decision Graphs), une variante des BDDs (Boolean Decision Diagrams) plus compacte. Les TDGs sont utilisés pour représenter aussi bien le domaine abstrait au cours de l'interprétation abstraite que les fonctions abstraites (qui servent à calculer la sémantique particulière d'un programme). Dans cette optique, nous avons donné une méthode générale pour étendre des représentations en TDG à des ordres supérieurs c'est-à-dire des représentations des fonctions sur les domaines de départ. Cette méthode peut permettre de trouver un codage des fonctions abstraites étant donné un codage des domaines abstraits. Il existe des fonctions pour lesquelles la représentation sous forme de TDG n'est pas compacte, ce qui peut consommer énormément d'espace mémoire, mais aussi de temps, car la plupart des opérations sur les TDGs dépendent de leur taille. La solution spécifique à l'interprétation abstraite est d'approximer ces fonctions par d'autres prenant moins de place. Cette approximation peut servir dans le cadre d'un opérateur d'élargissement dynamique si le domaine abstrait est codé, ou encore elle peut servir à approximer dès le départ les fonctions abstraites elles-mêmes, accélérant chaque itération. Comme exemple d'utilisation de ces différents procédés, on a codé l'analyse de nécessité, pour aboutir à un algorithme très performant, qui permet de trouver des résultats là où aucune analyse à la Mycroft exacte ne peut aboutir faute de place mémoire [255].
Il existe une classe de méthodes d'analyse de programmes basées sur l'usage de grammaires (introduite par N. Jones et S. Muchnick) ou sur celui de contraintes ensemblistes introduite par N. Heinze pour laquelle on a longtemps cru qu'il s'agissait de méthodes radicalement différentes de celles utilisées en interprétation abstraite. N. Heinze n'affirme-t-il pas, page 18 de sa thèse, que : << The finitary nature of abstract interpretation implies that there is a fundamental limitation on the accuracy of this approach to program analysis. There are decidable kinds of analysis that cannot be computed using abstract interpretation (even with widening and narrowing). The set-based analysis considered in this thesis is one example >>. Au contraire, nous avons montré que ces analyses basées sur l'approximation de langages formels par des grammaires ou des contraintes ensemblistes sont bien des interprétations abstraites isomorphes, avec calcul itératif de point fixe pour lequel on peut utiliser un élargissement, un transformateur de grammaires/contraintes finitaire ou même comme le fait implicitement N. Heinze de manière encore plus simple, un domaine abstrait qui est fini pour chaque programme particulier [243]. Cette nouvelle compréhension des analyses par grammaires ou contraintes a quelques avantages. En particulier le processus d'approximation est formalisé de manière rigoureuse et non plus expliqué en prenant quelques exemples. On met en évidence un domaine abstrait d'usage général qui peut être combiné avec d'autres domaines abstraites (polyèdres, congruences linéaires, etc.) pour analyser les valeurs numériques voire exprimer des conditions de contexte. Enfin, on montre que quelques affirmations sur les mérites respectifs de ces méthodes d'analyse et de l'interprétation abstraite sont pour le moins non justifiées [243].
Comme nous venons de le dire, une classe importante de méthodes d'analyse de programme est basée sur l'approximation de langages formels par des grammaires et/ou des contraintes ensemblistes. Malgré un usage largement répandu de ces objets, même en dehors du cadre de l'analyse de programmes, on ne sait pas manipuler efficacement les grammaires avec contraintes ensemblistes. Il s'agit de trouver de nouvelles représentations de tels objets, tout en développant des algorithmes de point fixe utilisant ces objets qui soient suffisamment efficaces pour être utilisables en pratique. L'utilisation d'approximations valides permet éventuellement de restreindre la taille des représentations au cours des calculs.
L'approche la plus générale du problème consiste à considérer ces grammaires comme des ensembles (presque) quelconques, éventuellement infinis, d'arbres éventuellement infinis. Pour que la représentation de ces arbres soit efficace, il faut d'une part qu'elle soit canonique (les tests d'égalités, très utilisés en recherche de point fixe doivent être rapides) et d'autre part compacte. Cela implique la recherche des cycles de l'arbre et leur repliage maximum. Une méthode a été développée qui permet de représenter des structures récursives selon leur pliage maximum, et cela au cours même de leur construction. Cette propriété est maintenue au cours des opérations récursives sur ces structures à un faible coût.
Une façon de représenter certains ensembles infinis d'arbres, et en particulier les grammaires, consiste à partager les branches d'arbres communes. On passe ainsi des ensembles aux relations. Or un arbre dont les feuilles sont des ensembles est une relation carrée, propriété qui ne se conserve pas lors des opérations d'union. Gérer directement des relations dans toute leur généralité, même en permettant des approximations, semble beaucoup trop complexe. Une approche semble donner un compromis acceptable : l'utilisation de la décomposition d'une relation en parties exactes. Une représentation des relations exactes a été mise au point dans le cadre des ensembles d'arbre. Elle permet facilement lorsque la relation devient trop complexe à gérer de l'approximer par au-dessus et par en-dessous par des relations plus simples. La décomposition en relations exactes n'étant pas unique, elle pose les problème de canonicité d'une part, et d'autre part de recherche de la décomposition optimale pour la représentation.
Un fois ces problèmes résolus, il faudra encore vérifier expérimentalement l'intérêt pratique de ces résultats jusqu'à présent entièrement théoriques.
Traditionnellement, le typage est une phase conceptuelle distincte de la définition de la sémantique dynamique du langage. Un système d'inférence de types peut se décomposer globalement comme suit : tout d'abord une algèbre de types, ensuite un ensemble de règles logiques affectant un type à chaque expression du langage, enfin un algorithme de reconstruction des types calculant le type le plus général d'une expression quelconque. Classiquement cet algorithme est basé sur l'algorithme d'unification de Robinson. Nous avons développé une autre approche qui consiste à comprendre le typage statique comme une interprétation abstraite d'une sémantique avec typage dynamique, que cette sémantique soit opérationnelle [276] ou dénotationnelle [227].
Ayant formulé les systèmes de type comme des interprétations abstraites [276], nous avons amélioré les algorithmes de typage classiques en utilisant les techniques d'élargissement de l'interprétation abstraite. Cette approche permet de relâcher les restrictions arbitraires des algorithmes classiques de typage comme la restriction monomorphe des constantes définies récursivement en ML. Pour illustrer le propos, considérons le système ML+ d'Alan Mycroft. Pour le système de types ML+, le problème d'inférence de types est indécidable. Dans le formalisme de l'interprétation abstraite, cela se traduit par un calcul du plus grand point fixe qui ne termine pas systématiquement [227, 276]. La solution classique à ce type de problèmes en interprétation abstraite consiste à introduire un opérateur d'élargissement pour accélérer la convergence. Nous avons exhibé toute une famille d'opérateurs d'élargissement qui modélisent le comportement de systèmes d'inférences déjà existants comme ceux de ML ou de Miranda, ou qui améliorent de façon substantielle les systèmes de types basés sur l'algèbre d'Hindley/Milner [276].
Un deuxième axe de recherche a consisté à combiner l'analyse de types avec d'autres types d'analyse. La combinaison de notre analyse avec les interprétations abstraites d'ensemble de valeurs numériques nous a permis :
Comme les types sont définis comme des valeurs abstraites, il est possible d'utiliser les types afin de représenter d'autres propriétés que celles habituellement utilisées en typage. Ainsi, nous nous sommes intéressés aux propriétés de l'analyse par nécessité pour les fonctions d'ordre supérieur en utilisant les méthodes initialement conçues pour les systèmes de types [259]. En fait, l'algorithme d'inférence obtenu fonctionne de manière satisfaisante, les résultats obtenus étant meilleurs que ceux de Kuo et Mishra.
Un troisième axe de recherche consiste à unifier les différents systèmes de types. Nous avons montré que notre modèle général permettait de modéliser les systèmes de types d'ordre supérieur. Dans un premier temps, nous nous sommes attaqués au système F (introduit par Girard et Reynolds) et il nous a été possible de montrer que ce système est une interprétation abstraite de la sémantique opérationnelle [258].
Très récemment, nous avons réussi à reconstruire la hiérarchie des systèmes de types du cube de Barendregt (à l'exception du calcul des constructions). Dans un autre domaine, il a été possible de définir une présentation générale uniforme des systèmes de types avec contraintes. Plus généralement, ces derniers systèmes sont très utiles pour la définition des systèmes de types pour des langages objets, puisqu'ils autorisent la prise en compte de dépendances dynamiques, ce que bien entendu les systèmes de types classiques ne sont pas en mesure d'appréhender. Un intérêt de la présentation par interprétation abstraite est de pouvoir exhiber les différentes restrictions syntaxiques qui ont été proposées par Fuh et Mishra, par Mitchell et par Henglein comme des opérateurs d'élargissement. En conclusion, nous montrons comment définir des opérateurs d'élargissement basés sur des critères sémantiques en lieu et place des critères syntaxiques, ce qui autorise la définition d'algorithmes de résolution de contraintes beaucoup moins grossiers.
L'intérêt théorique de ce résultat est d'avoir enfin une définition uniforme des systèmes de types du premier ordre et des systèmes de types d'ordre supérieur. Il permet de rompre la distinction entre typage ad hoc et typage paramétrique et permet de :
L'intérêt pratique de ce résultat est qu'il permet, grâce à une formalisation claire de l'abstraction, de définir des approximations décidables (c'est-à-dire non seulement l'algorithme termine mais trouve la solution de manière efficace) des systèmes de types d'ordre supérieur à l'aide des opérateurs d'élargissement. Des expérimentations sont en cours afin de déterminer les performances respectives des divers opérateurs actuellement étudiés pour le système F.
Une sémantique concrète décrit les comportements possibles d'un programme. Une sémantique abstraite fait de même en considérant des propriétés approchées du contrôle de l'exécution. Cette sémantique est généralement paramétrée par un domaine abstrait formalisant les propriétés considérées pour les objets manipulés par le programme.
L'analyse de nécessité (strictness analysis) est
traditionnellement basée sur une sémantique dénotationnelle dans
laquelle les propriétés des fonctions 
s'expriment par un élément de 
. Cette
approche ne permet pas de rendre compte de nombreuses autres
méthodes d'analyse (par exemple l'analyse de projection de J.
Hughes et P. Wadler) comme étant des interprétations abstraites.
Une première raison est que certaines propriétés (comme
l'absence traduisant la non-utilisation d'un paramètre) ne
s'expriment pas comme un élément de mais
plutôt comme un élément de 
. Une seconde
raison vient du fait que les sémantiques dénotationnelles
correspondent à des approximations où des informations
essentielles sur le déroulement des calculs sont perdus, ce qui
n'est pas le cas des sémantiques relationnelles
[287] et opérationnelles étendues à des
comportements infinis [267]. Pour traiter ces
problèmes nous avons généralisé l'approche des correspondances
de Galois aux interprétations abstraites d'ordre supérieur en
distinguant ordre partiel d'approximation et pré-ordre de calcul
[225].
L'analyse de comportement, introduite dans [225], combine les analyses de programmes fonctionnels ne dépendant pas des valeurs manipulées par le programme. Ceci recouvre l'analyse de nécessité, l'analyse de terminaison à la Mycroft, l'analyse de projection (J. Hughes et P. Wadler), l'analyse d'équivalence partiel (PER analysis de S. Hunt), l'analyse de temps de liaison (binding time analysis), etc. Ce type d'analyse est utilisé pour la compilation de langages paresseux (pour transformer des appels par nécessité/par nom par des appels par valeurs qui sont nettement plus efficaces) et l'évaluation partielle (pour effectuer des calculs dès la compilation).
Un problème récurrent de l'analyse de nécessité est celui de l'efficacité. Comme exemple d'utilisation des TDGs, nous avons codé l'analyse de nécessité, pour aboutir à un algorithme très performant, qui permet de trouver des résultats là où aucune analyse à la Mycroft exacte ne peut aboutir faute de place mémoire [255].
L'analyse de nécessité traditionnelle comme ci-dessus est basée sur des domaines booléens simples pour lesquels les ordres abstraits d'approximation et de calcul coïncident. Ce n'est pas le cas pour les analyses de comportement [225] dans laquelle on sépare les éléments statiques (pour lesquelles la terminaison est certaine) des éléments dynamiques (pour lesquels la non-terminaison est possible). La situation est alors compliquée par le fait qu'un pré-ordre de calcul conduit à un ensemble de solutions abstraites possibles dont il s'agit d'extraire les plus précises.
Pour étudier ce phénomène, nous avons étudié la combinaison
de l'analyse de nécessité (strictness analysis) et des temps de
liaison (binding time analysis) [289, 261]
pour un petit langage fonctionnel paresseux. Cette combinaison
permet de trouver des résultats significatifs alors qu'elles
échoueraient séparément. Le produit précision 
vitesse
d'analyse est à l'avantage de l'analyse combinée : le treillis
abstrait est beaucoup plus grand que la somme disjointe des deux
treillis utilisés pour l'analyse de nécessité et des temps de
liaison, et les premières itérations de ces deux analyses sont
communes. L'usage de correspondances de Galois relatives à une
sémantique opérationnelle permet de caractériser exactement la
perte d'information dans l'analyse.
Il est facile d'intégrer des analyses abstraites inférant des
propriétés de la logique du premier ordre (pour exprimer
terminaison sure, la non-terminaison sure, la dépendance par rapport
à des variables dont nous ne savions rien, etc.). Le fait de mettre
la non-terminaison au même niveau que la terminaison dans le
treillis abstrait nous empêche d'abstraire directement une fonction
définie récursivement (donc par un plus petit point fixe pour un
ordre où non-terminaison 
terminaison). Ce problème
a été résolu en définissant des itérations abstraites qui
contiennent toujours l'abstraction des itérations concrètes de
notre fonction (du moins pour un nombre fini d'itérations). Le
passage à la limite se justifie par le fait que nous inférons des
propriétés de la logique du premier ordre, et qu'ainsi il existe
un sous-modèle fini sur lequel les itérés abstraits sont
également valables.
Ensuite, ce travail a été élargi de manière à pouvoir énoncer des propriétés générales concernant le comportement d'un programme, et en particulier celui de ses fonctions (terminaison, valeur, structures de données, types). Le langage initial a été élargi à l'ordre supérieur pour des structures de données arbitraires, avec la possibilité de distinguer des structures arbitrairement grandes, mais finies, des structures infinies. Cela a nécessité l'introduction de preuves de terminaison totales dans le cadre de l'interprétation abstraite, et l'introduction d'une fonction d'abstraction correspondant à la preuve du théorème de Tarski.
L'analyse doit maintenant être généralisée de manière à pouvoir traiter des langages de programmation réels : en pratique, cela consiste à donner le comportement d'un programme impératif avec tous les effets de bords qu'il est susceptible de générer. L'intérêt serait d'analyser des programmes écrits dans un petit langage orienté-objet. Les propriétés dégagées peuvent servir soit au compilateur, soit être délivrées en l'état au programmeur, ce qui lui fournit un metteur au point abstrait.
Ce travail est basé sur une sémantique opérationnelle des petits pas de programmes PROLOG (résolution SLD). Les principales contributions concernent l'usage de domaines abstraits infinis (les analyses classiques utilisent des treillis finis), en particulier des langages formels, grammaires et contraintes ensemblistes [238] et la combinaison des analyses descendantes et ascendantes (les analyses classiques utilisent l'une ou l'autre mais pas les deux) [236].
Certaines analyses fines de programmes parallèles comme l'exclusion mutuelle ou l'indépendance et la validation de propriétés liées à la géométrie des systèmes de transitions (blocages, branchements, etc.) requièrent l'usage de sémantiques qui décrivent véritablement le parallélisme entre processus concurrents à l'aide d'automates munis de transitions de dimension supérieure. Ces automates nous permettent de définir des sémantique approchées, calculables par interprétation abstraite en vue de l'analyse statique des programmes parallèles considérés. Cela a été réalisé pour différents types de langages (Linda, Parallel Pascal, CML) et une propriété de correction sémantique de l'interprétation abstraite a été prouvée. Deux techniques différentes permettent d'atteindre cet objectif :
Une caractérisation des interprétations abstraites entre deux automates de dimension supérieure a été donnée en terme d'adjonctions. La troncation est une adjonction qui permet de modéliser la sémantique d'un pool de n processeurs qui entrent en compétition afin d'exécuter un programme. Les repliements d'états permettent de simplifier les configurations abstraites et de rendre la sémantique approchée calculable statiquement.
L'implantation d'un analyseur de Parallel Pascal basé sur une telle sémantique a été effectuée et est disponible sur le serveur WEB du DMI. Certaines techniques d'implémentation comme l'utilisation de transitions d'un grain plus grossier que dans les définitions sémantiques (Virtual Coarsening) permettent l'interprétation abstraite précise de programmes de taille raisonnable car elles diminuent fortement (au moins d'un facteur 4) le nombre d'états à considérer. Pour des algorithmes classiques d'exclusion mutuelle comme ceux de Dekker ou de Peterson, la preuve d'invariance est ainsi réalisée par l'interprète abstrait en quelques secondes de calcul. L'automate abstrait qui en résulte compte un millier d'états alors que le nombre d'états réels de ce programme est de l'ordre de cent mille. On gagne donc un facteur 100 sur la vérification de la propriété d'exclusion mutuelle dans cet exemple significatif [247].
D'autres programmes (avec des sémaphores par exemple) ont été analysés avec succès. L'analyseur adjoint au source du programme des invariants calculés à chaque point de contrôle. Il produit aussi l'automate qu'on peut visualiser ou bien fournir comme input à une deuxième passe d'analyse.
La vérification de modèle (model-checking) est une technique séduisante puisque, contrairement à l'interprétation abstraite, elle fournit des résultats exacts. Malheureusement, et contrairement à l'interprétation abstraite, elle n'aboutit pas toujours, faute de temps, d'espace mémoire ou parce qu'il faut explorer exhaustivement un espace d'états infini. La vérification de modèle de modèle et l'analyse de programme par interprétation abstraite apparaissent donc comme complémentaires. Nous avons montré comment les combiner dans un calcul parallèle [244], l'analyse du système, convenablement conduite en parallèle avec la vérification du modèle permettant de réduire l'espace des états devant être effectivement explorés. Dans cette combinaison l'analyse est approchée et le model-checking est exact de sorte que la terminaison n'est toujours pas assurée. Une autre approche, celle du model-checking abstrait est également explorée, pour garantir la terminaison au prix d'une perte de précision.
L'idée du model-checking abstrait est de valider les formules de logique modale qui caractérisent certaines propriétés comme les blocages (deadlocks), l'équité ou l'exclusion mutuelle sur les systèmes de transitions approchés obtenus par interprétation abstraite, et d'en tirer une information sur la sémantique concrète. En effet, contrairement au model-checking traditionnel, le système de transitions d'un programme n'est pas calculable en général [246, 248].
On peut quand même tirer parti du fait qu'il existe d'excellents
algorithmes de model-checking sur les automates. La difficulté
principale est de réussir à transférer la validité d'une
formule de logique temporelle suffisamment expressive de la
sémantique abstraite vers la sémantique standard. Ce résultat a
été obtenu pour le 
-calcul complet grâce à une
interprétation abstraite qui allie à la fois une approximation
supérieure et une approximation inférieure des états concrets.
Un évaluateur de formules logiques du -calcul est en ce moment
testé en sortie de l'interprète abstrait pour réaliser un outil
plus général d'analyse de programmes parallèles.
Dans le modèle des automates de dimension supérieure, on a la
possibilité de distinguer de façon très fine les ordonnanceurs
possibles d'un programme parallèle tournant sur une machine
contrainte (nombre de processeurs limité, topologie de communication
imposée, exclusion mutuelle obligatoire pour certains
objets 
). Toutes ces conditions contraignent les exécutions
possibles et on peut donner des critères géométriques
(homotopie) pour déterminer s'il y en a encore
(spécification/vérification) et même pour déterminer les
meilleures possibles. A contrario, on peut aussi essayer de
paralléliser au maximum un programme séquentiel afin d'occuper au
maximum un type de machine donné. Ces deux problèmes se posent en
des termes géométriques similaires, et sont naturellement
exposés dans le cadre de l'interprétation abstraite
[251].
Nous avons commencé à nous intéresser aux applications des sémantiques du vrai parallélisme par automates de dimensions supérieures aux protocoles de systèmes distribués tolérants aux pannes. Un premier travail a permis de lier les considérations géométriques des automates de dimension supérieure à celles de M. Herlihy, N. Shavit et S. Rajsbaum concernant les systèmes distribués t-résilients (résistants à t pannes). Cela a permis de prouver à nouveau de façon sémantique un résultat de calculabilité sur les systèmes t-résilients à mémoire partagée (avec lecture et écriture atomique). Cette nouvelle vision des choses a rendu possible l'amélioration de l'algorithme d'Herlihy pour la génération automatique de protocoles sans attente [253], ainsi que la généralisation à d'autres systèmes (avec test & set etc.).
Nous avons étendu le 
-calcul par des informations stochastiques
qui donnent un modèle uniforme avec lequel il est possible
d'étudier des propriétés qualitatives (comportements) et
quantitative (performances) des systèmes parallèles et distribués.
À titre d'analyse de cas, nous avons étudié les procédures de
transmission dans les réseaux de téléphonie mobile
[282].
L'objet de cette recherche, commencée récemment, est de définir un cadre sémantique pour l'interprétation abstraite des langages orientés objets. Les applications envisagées concernent le typage, l'optimisation dans les compilateurs (par exemple pour transformer des appels à des fonctions virtuelles en appels statiques) et la mise au point abstraite (où les valeurs utilisées pour la mise au point interactive sont abstraites c'est-à-dire à des ensembles de valeurs concrètes qu'il faudrait considérer individuellement dans les approches classiques).
Les perspectives doivent être situées dans le contexte fixé par le DMI. La croissance des surfaces occupées et du nombre de chercheurs est nulle, ce qui pose à la fois le problème de masse critique et d'accueil des post-doctorants (programme européen CHM), années sabbatiques, etc. L'équipe est largement constituée de jeunes chercheurs thésards dont le renouvellement est rapide et qui quittent l'équipe quand ils atteignent leur maturité scientifique. En dehors du responsable, il n'y a pas de chercheurs confirmés et d'ingénieurs de recherche affectés à des projets scientifiques à moyen terme, ce qui limite considérablement les possibilités de développements pratiques et du suivi de ces développements. La durée de vie de l'équipe, comme toutes celles du DMI, est limitée dans le temps, etc. Ces conditions de travail nous placent dans une position de relative faiblesse par rapport à nos partenaires et concurrents européens.
Malgré ces conditions difficiles, l'objectif essentiel est de fournir un excellent cadre de travail aux jeunes thésards. Nos atouts sont la qualité des chercheurs, des thèmes de recherche, des indispensables partenaires extérieurs et de l'animation scientifique que créent le séminaire et les visiteurs extérieurs.
En ce qui concerne nos idées sur la sémantique et l'interprétation abstraite, elles se répandent doucement mais sûrement, notamment au travers d'écoles pour jeunes chercheurs :
dans des congrès
ICCL'94 [234], GULP-PRODE'95 [237], CAV'95
[235], POPL'97 [227], MFPS XIII
[240], SAS'97 ou réunions thématiques (workshops)
WAILL'95 [236], 4th Compulog [238], Venice
workshop'95 [239], F.N.R.S. meeting [241].
Un certain nombre d'éléments prospectifs ont déjà été évoqués dans le compte-rendu du travail des quatre dernières années. Nous comptons nous concentrer sur quelques thèmes, comme par exemple :