0.1  Equipes de recherche

0.1.1  Équipe Sémantique et Interprétation Abstraite


Part 1
Activité scientifique des équipes


Chapter 1
Équipe Sémantique et Interprétation Abstraite

L'équipe s'est constituée en octobre 1991 à l'occasion du recrutement comme professeur de Patrick Cousot. Elle conserve des liens privilégiés avec l'équipe "Sémantique, preuve et interprétation abstraite" du LIX, qu'il a créée et dirigée jusqu'au 1er octobre 1991, au travers d'un séminaire hebdomadaire.

1.1  Introduction

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.
Les modèles de sémantiques :   ce travail concerne principalement les méthodes de présentation des sémantiques, l'étude des relations entre sémantiques permettant de construire des hiérarchies de descriptions obtenues par approximation et les modèles géométriques du parallélisme permettant une distinction fine entre vrai parallélisme et non-déterminisme
Les fondements de l'interprétation abstraite :   il s'agit d'étudier les diverses modélisations de la notion d'approximation discrète en sémantique. Les applications concernent la sémantique (par exemple le non-déterminisme peut être compris comme une approximation du parallélisme) et l'analyse de programme (par exemple l'analyse de nécessité pour les langages fonctionnels paresseux est traditionnelement comprise comme une approximation de leur sémantique dénotationnelle).
Les méthodes d'analyse et de manipulation de programmes par interprétation abstraite de sémantiques :   il s'agit de spécifier et de construire des analyseurs sémantiques pour la détermination automatique, statique et correcte de propriétés dynamiques des programmes. L'analyse sémantique de programmes peut s'organiser en deux parties relativement indépendantes. Cette dichotomie sert de base à la présentation de notre travail. Les applications, qui concernent la mise au point symbolique de programmes, la compilation, l'évaluation partielle, la transformation de programmes comme la parallélisation, les preuves (génération automatique d'invariants, preuves de terminaison), etc., sont évidemment liées aux deux aspects. Les efforts ont porté principalement sur les langages fonctionnels (analyse de nécessité, des temps de liaison, typage), les langages logiques, l'analyse de programmes parallèles et plus récemment l'analyse des langages objets.

1.2  Sémantiques

1.2.1  Présentation de sémantiques et construction de hiérarchies de sémantiques par interprétation abstraite

Si toutes les méthodes de définition de sémantiques des langages de programmtion 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 [19,11,14], ce qui permet alors de montrer l'équivalence de ces divers modes de présentation [50,8]. Ces présentations de sémantiques étant conservées par interprétation abstraite [50,8], 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 [19,11,14] qui diffèrent seulement par la précision de la description de l'exécution et le mode de présentation. Par exemple [38] 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 [9]. 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.

1.2.2  Méthodes géométriques pour le parallélisme

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. 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). 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.
On voit déjà dans cet exemple 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 deadlocks, les branchements et confluences, et donc les équivalences sémantiques "branching-time" [24], l'ordonnancement des actions 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 [25]. 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. Il en découle naturellement des algorithmes qui devrons être expérimentés dans un avenir proche. D'autre part, les moyens de calculs inventés pour la topologie algébrique (suites exactes, suites spectrales) prennent un tour tout particulier qu'il est intéressant d'examiner. Cela est d'autant plus vrai que les objets que nous étudions sont quelque peu différents de leurs homologues mathématiques classiques.
Tout ceci ne serait pas complet si on ne démontrait pas que l'on peut donner des sémantiques de languages dans les automates de dimension supérieure. Nous avons prouvé qu'il est possible de donner des sémantiques à la SOS ainsi que des sémantiques catégoriques compositionnelles [25,21]. Les automates de dimension supérieure fournissent également un modèle de la logique linéaire intuitioniste. D'autres logiques (temporelles, ) peuvent être utilisées en liaison avec ce modèle et devraient fournir des moyens de spécification/vérification de programmes parallèles (éventuellement par systèmes de types).
Enfin, 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 [46], et les systèmes probabilistes. Nous n'avons encore qu'effleuré ces sujets, mais nous avons déjà montré comment obtenir des sémantiques opérationnelles vraiment parallèles, temps réel (éventuellement continu). 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.

1.3  Interprétation abstraite

1.3.1  Fondements de l'interprétation abstraite

La correspondance entre les propriétés concrètes et abstraites s'établit traditionnellement par une correspondance de Galois [13]. Ceci correspond au cas où toute propriété concrète a une meilleure approximation dans le domaine de propriétés abstraites. Cette propriété est très intéressante car la sémantique concrète et l'approximation définie par la correspondance de Galois définit entièrement la sémantique qui se déduit constructivement de la sémantique concè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 [4,16]. Ceci conduit à définir des notions de complétude relatives à divers degrés d'abstraction [18].
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ésulats 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:'esolus grossièrement [35,36,5].
Comme évoqué précédemment, les techniques d'analyse sémantique de programmes ont été principalement présentées sont formes de points fixes ou équationnelles. Depuis peu, la présentation sous forme de règles est plus courante. Nous avons introduit GSOS, une généralisation de SOS pour décrire des comportements infinis [19] 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 [50].

1.3.2  Analyse sémantique de programmes

Domaines abstraits

L'étude d'un domaine abstrait consiste à imaginer un modèle mathématique de propri\' etés de programmes. Pour être utilisable pour l'analyse automatique de programmes, il faut en concevoir une repé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.
Utilisation des congruences arithmétiques en interprétation abstraite   Nous avons étudié les propriétés de congruence linéaire permettant de lier les valeurs entières ou rationnelles x1, ..., xn de variables X1, ..., Xn d'un programme sous la forme a1 x1 ++an xn b[m] où a1, ..., an, b and m sont des constantes déterminées automatiquement par l'analyse [27]. On peut ainsi exprimer indirectement des propriétés de régularité dans les programmes, par exemple dans une structure de données (en comptant une position dans cette structure) ou lors de communications sur un canal (en liant le rang de la communication à une propriété de l'objet transmis.
Utilisation des BDDs en interprétation abstraite   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 variantes 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 [55,29]. Une application est prévue en collaboration avec N. Halbwachs en vérification de modules.
Utilisation des langages formels, grammaires et contraintes ensemblistes en interprétation abstraite   Il existe une classe de méthodes d'analyse de programmes basées sur l'usage de grammaires (introduit par N. Jones et S. Muchnick) ou sur celui de contraintes ensemblistes introduit 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 languages 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 [20]. 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 (polyhè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 [51,20].
Dans cette ligne, une recherche sur la construction de nouvelles représentations pour des ensembles infinis en interprétation abstraite vient de commencer. Il s'agit de trouver des représentations efficaces, en particulier du point de vue du calcul de point fixe, à des ensembles typiquement définis par des grammaires, auxquelles on ajoute la possibilité d'avoir des intersections, des projections et des négations.
Combinaisons de domaines abstraits   Il est intéressant de combiner des domaines abstraits pour décomposer une propriété complexe en éléments simples ou pour rassembler des analyses de programmes conçues indépendamment. Diverses études de réductions et complétions sont faites dans [47,3,17,28].
Typage par interprétation abstraite  
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 un domaine abstrait c'est-à-dire une algèbre de types, ensuite un ensemble de règles logiques assignant à chaque expression du langage un type, enfin un algorithme de reconstruction des types calculant pour chaque expression le type le plus général. Classiquement cet algorithme est basé sur l'algorithme d'unification de Robinson. Une autre approche consiste à utiliser l'interprétation abstraite. Les travaux d'Alan Mycroft et de Neil Jones ont, en 1984, ouvert la voie. Cependant, certaines difficultés font que cette approche connaît un relatif succès uniquement dans le typage de Prolog. Dans le domaine des langages fonctionnels, cette approche n'a connu,à quelques exceptions près, que peu de développements.
Initialement, nous nous étions fixé comme objectif d'étudier les parallèles entre les systèmes de règles d'inférence et les systèmes de types obtenus par interprétation abstraite. Cependant, au cours de l'évolution des travaux, il a nous a été possible de montrer que les systèmes d'inférence de types classiques pouvaient être reformulés en utilisant l'interprétation abstraite [39]. Il n'était dès lors plus possible de dire qu'une approche était meilleure que l'autre, puisqu'il nous a été possible de montrer que les résultats obtenus par les systèmes de types pouvaient être obtenus par interprétation abstraite. Ceci nous permet d'enrichir les théories de types existantes avec la théorie et les techniques de l'interprétation abstraite.
En effet, il nous a été possible de définir un type comme valeur abstraite de l'ensemble des valeurs que le programme peut être amené à manipuler. En fait, la définition n'est pas immédiate et nécessite de décomposer l'abstraction en deux abstractions distinctes. La première transformation consiste à abstraire l'ensemble des valeurs par des "types abstraits" dénotant une approximation supérieure de cet ensemble. Toutefois, étant donné la taille gigantesque du treillis de types que nous avons du définir précédemment, il a été nécessaire de nous restreindre à une approximation de ce dernier. La seconde approximation consiste donc à sélectionner certains sous-ensembles de ces types abstraits et d'effectuer une projection vers ces sous-ensembles. Dans ce modèle, à l'opposé de la démarche classique, la notion de "type principal" est caractérisée - c'est-à-dire la notion de type le moins restrictif pour l'expression donnée tout en assurant la correction de l'exécution - par un plus grand point fixe.
Si nous décidons de nous restreindre à l'algèbre de types de ML, nous pouvons démonter que le système d'inférence de types que nous obtenons en utilisant la méthode précédemment introduite est équivalent au système ML+ d'Alan Mycroft. Pour le système de types ML+, le problème d'inférence de types est indécidable. En conséquence, le calcul du plus grand point fixe ne termine pas systématiquement. Tout d'abord, nous avons développé des méthodes autorisant l'introduction d'un opérateur d'élargissement permettant d'accélérer la convergence de l'algorithme de typage et d'en assurer la terminaison. Finalement, nous avons exhibé toute une famille d'opérateurs d'élargissement soit modélisant le comportement de systèmes d'inférences déjà existants comme ceux de ML ou de Miranda, soit améliorant de façon substantielle les systèmes de types basés sur l'algèbre d'Hindley/Milner [31,33,32,40].
De plus, il nous a été possible de nous caractériser des systèmes de types beaucoup plus puissants, comme les types fractionnels [30], les systèmes de types de Coppo-Dezani ainsi que les système F de Girard par interprétation abstraite. Actuellement, nous cherchons à définir des opérateurs d'élargisemment nous permmettant d'exhiber un sous-ensemble non trivial décidable de ces deux systèmes de types.
Système d'analyses par règles d'inférences construites par interprétation abstraite   Ayant démontré qu'il est possible de considérer un type comme une valeur abstraite particulière, il est maintenant possible d'introduire des "types" modélisant les propriétés normalement décrites par des modèles de valeurs absraites utilisées en interprétation abstraite. Pour l'instant, nous nous sommes intéressés aux propriétés utiles pour l'analyse de nécessité (strictness analysis, c'est-à-dire une analyse qui détermine les arguments d'une fonction dont l'evaluation immédiate ne change pas le comportement de la fonction) [34]. Ceci nous a permis de concevoir un système d'inférence des propriétés de nécessité pour des langages fonctionnels typés ou non typés d'ordre supérieur. Nous envisageons d'étendre le modèle aux propriétés utilisées pour l'analyse de temps de liaison (binding time analysis, c'est-à-dire une analyse qui détermine les parties d'un programme qui peuvent être évaluées au moment de la compilation).
Extension des systèmes de types   Un intérêt d'utiliser l'interprétation abstraite afin de défininir des système de types est de pouvoir combiner l'analyse de types avec d'autres types d'analyse. La combinaison de notre analyse avec les interprétations abstraites d'ensembles de valeurs numériques nous a permis de développer un système de types pour un langage ML parallèle autorisant l'existence de canaux non typés. Ce système de types est basé sur la combinaison de l'algorithme d'inférence de types par interprétation asbtraite et un algorithme d'analyse des communications. L'analyse de communication nous permet de déterminer de manière approchée l'ensemble des valeurs (ou plus exactement de leurs types) transitant en un point d'émission et un point deréception du programme. Ceci nous permet d'inférer les divers types des valeurs reçues à partir des types des valeurs envoyées. De même, nous avons développé un système de types pour les listes hétérogènes, c'est-à-dire des listes comprenant des valeurs de types différents.

Sémantiques abstraites

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'ees pour les objets manipulés par le programme.
Analyse sémantique de programmes fonctionnels d'ordre supérieur par interprétation abstraite   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 f D1 D2 s'expriment par un élément de (D1)(D2). 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 (D1)(D2) mais plutôt comme un élément de (D1 D2). 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 [37] et opérationnelles étendues à des comportements infinis [19]. 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 [7].
Analyse de projection   Ces recherches formalisent l'analyse par projections de J. Hughes et P. Wadler dans un cadre d'interprétation abstraite, la comparent à l'analyse par idéaux et l'appliquent à un langage de premier ordre avec des types de données récursifs [53].
Le treillis abstrait de projections qui a été défini présente la particularité d'être disjonctif et non-uniforme : sont donc bien représentées les propriétés respectivement des fonctions à plusieurs arguments et du contenu des structures de donnés récursives comme les listes. Un opérateur d'élargissement est utilisé pour obtenir des classes de propriétés uniformes.
Analyse de comportement par interprétation abstraite   L'analyse de comportement, introduite dans [7], 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).
L'analyse de nécessité peut être obtenue par interprétation abstraite de programmes fonctionnels basée sur une sémantique par réduction de graphes [54,2,1] ou relationnelles [6,49]. Un problème récurrent 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 [55,29].
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 [7] 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) [56]. Cette combinaison permet de trouver des résultats significatifs alors qu'elles échoueraient séparement. 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 dependance 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 \sqsubseteq 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 iterés abstraits sont également valables.
Analyse sémantique de programmes logiques par interprétation abstraite   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) et la combinaison des analyses descendantes et ascendantes (les analyses classiques utilisent l'une ou l'autre mais pas les deux) [3,15,17].
Analyse sémantique de programmes parallèles par interprétation abstraite  
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. Cette dimension décrit le degré de parallélisme effectif lors de l'exécution d'opérations concurrentes.
On peut définir diverses sortes de systèmes de transitions de dimension supérieure. Les systèmes totaux 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 permettent de plus de modéliser l'interférence entre plusieurs actions parallèles.

   Programmes parallèles communicants  
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, Concurrent Pascal, CML) et une propriété de correction sémantique de l'interprétation abstraite a été prouvée [21]. 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.
En ce moment, une implémentation d'un prototype d'un analyseur de Concurrent Pascal basée sur une telle sémantique est en cours. 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 d'envisager l'interprétation abstraite précise de programmes de taille raisonnable.

   Logique temporelle et model-checking abstrait  
L'idée du model-checking abstrait est de valider les formules de logique modale qui caractérisent certaines propriétés comme les interblocages (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.
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 est obtenu pour le m-calcul complet grâce à une interprétation abstraite qui allie à la fois une approximation supérieure et une approximation inférieure des états concrets [23].

   Ordonnancement 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 [26]. Tout ceci n'a pas encore été fait en toute généralité et se trouve donner des idées d'algorithmes d'analyse statique par interprétation abstraite qui doivent encore être développés, pour aider à la vérification de programmes parallèles ainsi que pour améliorer les performances de certains compilateurs. Nous désirerons également développer un lien avec les travaux (méthodes géométriques) de M. Herlihy, N. Shavit, M. Saks, H. Attiya sur les protocoles de systèmes distribués, et ceux de J. Gunawardena sur les bases de données parallèles. Nous sommes proches d'un traitement sémantique de ces questions, en utilisant le modèle des automates de dimension supérieure et de bonnes notions géométriques.
Analyse sémantique de langages orientés objets par interprétation abstraite   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).

Part 2
Eléments d'appréciation de l'activité du laboratoire


Chapter 2
Collaborations

2.1  Sémantique et Interprétation Abstraite

Chapter 3
Missions, conférences et séminaires

3.1  Sémantique et Interprétation Abstraite

Chapter 4
Accueil de chercheurs

4.1  Sémantique et Interprétation Abstraite

Professeurs et directeurs de recherche invités

Chapter 5
Diffusion de la connaissance

5.1  Sémantique et Interprétation Abstraite

Chapter 6
Réalisation et diffusion de logiciels, brevets

6.1  Sémantique et Interprétation Abstraite

6.1.1  Brevets

É. Goubault est le premier inventeur des brevets européens numéro 91480054.5 "A vector quantizing method for coding signals and system for implementing said method" (en date du 29/03/91 déposé pour IBM France, puis breveté aux Etats-Unis) et numéro 92480097.2 "Improved method for coding digital data using vector quantizing techniques and device for implementing said method" (en date du 30/06/92 déposé pour IBM France).

6.1.2  Réalisation et diffusion de logiciels

Compilation des langages fonctionnels de Cridlig   Ce travail commencé dans l'équipe ICSLA de l'INRIA-Rocquencourt a débouché sur la réalisation effective d'un compilateur optimisant et portable pour le langage Caml-Light (un des deux dialectes dominants de ML). Ce compilateur Camlot a été distribué sur le réseau Internet et est utilisé par bon nombre de développeurs Caml-Light [22].
Ce compilateur inaugure une nouvelle voie dans la compilation des langages fonctionnels. En effet, il traduit le flot de contrôle d'un langage fonctionnel d'ordre supérieur vers les constructions efficaces d'un langage impératif du premier ordre, en l'occurrence le langage C. Cette traduction est effectuée directement de fonction ML à fonction C. Les valeurs fonctionnelles sont traduites en fermetures, et une analyse statique est effectuée pour déterminer les variables liées à passer dans les environnements au cours de l'exécution. Une analyse similaire permet de décider si une fonction ML peut être intégrée à une fonction C ou bien si elle doit être déplacée au niveau supérieur (toplevel). Quant aux structures de données dynamiques de ML, elles sont allouées dans le tas C par un gestionnaire de pages mémoires et récupérées automatiquement grâce à un ramasse-miettes (garbage collector) conservatif.

Chapter 7
Évaluation de la recherche

7.1  Sémantique et Interprétation Abstraite

Chapter 8
Encadrement doctoral

8.1  Direction de thèses

Nous donnons uniquement la liste des thèses soutenues entre 1991 et 1995 et dirigées par un membre du laboratoire.

8.2  Participation à d'autres jurys de thèses

Chapter 9
Enseignement

9.1  2èmecycle

9.1.1  En France

9.2  3èmecycle

9.2.1  En France

Chapter 10
Distinctions honorifiques

10.1  Contrats

10.1.1  Équipe "Sémantique et interprétation abstraite"

Bibliography

Livres
[1]
Goubault (É.), Hankin (C.), van Eekelen (M.) et Nocker (E.). - Abstract reduction: towards a theory via abstract interpretation. In : Term Graph Rewriting: Theory and Practice, éd. par Sleep (R.), Plasmeijer (R.) et van Eekelen (M.), chap. 9, pp. 117-129. - John Wiley & Sons, Ltd., 1993.
[2]
Goubault (É.) et Hankin (C.). - A lattice for the abstract interpretation of term graph rewriting systems. In : Term Graph Rewriting: Theory and Practice, éd. par Sleep (R.), Plasmeijer (R.) et van Eekelen (M.), chap. 10, pp. 131-140. - John Wiley & Sons, Ltd., 1993.
Articles invités
[3]
Cousot (P.) et Cousot (R.). - Abstract interpretation and application to logic programs. Journal of Logic Programming, vol. 13, n'27 2-3, 1992, pp. 103-179.
[4]
Cousot (P.) et Cousot (R.). - Abstract interpretation frameworks. Journal of Logic and Computation, vol. 2, n'27 4, août 1992, pp. 511-547.
[5]
Cousot (P.) et Cousot (R.). - Comparing the Galois connection and widening/narrowing approaches to abstract interpretation, papier invité. In : Programming Language Implementation and Logic Programming, Proceedings of the Fourth International Symposium, PLILP'92, éd. par Bruynooghe (M.) et Wirsing (M.), pp. 269-295. - Springer-Verlag, Berlin, Allemagne, 1992.
[6]
Cousot (P.) et Cousot (R.). - Galois connection based abstract interpretations for strictness analysis, papier invité. In : Proceedings of the International Conference on Formal Methods in Programming and their Applications, éd. par rner (D. Bjø), Broy (M.) et Pottosin (I.V.), pp. 98-127. - Springer-Verlag, Berlin, Allemagne, juin 28-juillet 2, 1993.
[7]
Cousot (P.) et Cousot (R.). - Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages), papier invité. In : Proceedings of the 1994 International Conference on Computer Languages. pp. 95-112. - IEEE Computer Society Press, Los Alamitos, Californie, U.S.A., mai 16-19, 1994.
[8]
 *  Cousot (P.) et Cousot (R.). - Compositional and inductive semantic definitions in fixpoint, equational, constraint, closure-condition, rule-based and game-theoretic form, papier invité. In : Computer Aided Verification, Proceedings of the 7th International Conference, CAV'95, éd. par Wolper (P.). - Springer-Verlag, Berlin, Allemagne, juillet 1995. À paraître.
Articles dans des revues internationales avec comité de lecture
[9]
Cousot (P.) et Cousot (R.). - "A la Burstall" intermittent assertions induction principles for proving inevitability properties of programs. Theoretical Computer Science, vol. 120, 1993, pp. 123-155.
[10]
Goubault (É.) et Lebris (C.). - Groupes ext1 et déformations de représentations de certaines algèbres de lie nilpotentes. Bulletin des Sciences Mathématiques, vol. 2ème série, n'27 116, 1992.
Conférences invitées
[11]
Cousot (P.) et Cousot (R.). - Constructing a hierarchy of semantics of functional programs by abstract interpretation, conférence invitée. In : Workshop on Static Analysis, WSA'92. - Bordeaux, France,  23-25 septembre 1992.
[12]
Cousot (P.) et Cousot (R.). - Abstract interpretation of parallel programs, conférence invitée. In : Int. Kolloquium, Sonderforschungsbereich 124, VLSI - Entwurfsmethoden und Parallelität. - Sarrebrücken, Allemagne, 2-3 septembre 1993.
[13]
Cousot (P.) et Cousot (R.). - Galois connections and abstract interpretation, conférence invitée. In : Mathematics of Programming Workshop on Galois Connections. - Universiteit Utrecht, Pays-bas, 13-14 septembre 1993.
[14]
Cousot (P.) et Cousot (R.). - Inductive definitions of semantics and connections between semantics as used in abstract interpretation, conférence invitée. In : MASK Meeting. - Koblenz, Allemagne, 6-8 octobre 1993.
[15]
Cousot (P.). - Abstract interpretation of logic programs, invited advanced tutorial. In : Proceedings of the 8th International Conference on Logic Programs, éd. par Furukawa (K.). p. 940. - Paris, France, 25-28 juin 1991.
[16]
Cousot (P.). - A tutorial on abstract interpretation,. In : 1994 International Conference on Computer Languages. - mai 16-19, 1994.
[17]
Cousot (P.). - Combining bottom-up and top-down in abstract interpretation of logic languages, conférence invitée. In : Special Workshop on Abstract Interpretation of Logic Languages. - juin 18-19 1995.
[18]
Cousot (P.). - Completeness in abstract interpretation, conférence invitée. In : GULP-PRODE'95. - septembre 1995.
Communications dans des conférences internationales avec comité de lecture
[19]
Cousot (P.) et Cousot (R.). - Inductive definitions, semantics and abstract interpretation. In : Conference Record of the 19th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 83-94. - Albuquerque, Nouveau Mexique, 1992.
[20]
 *  Cousot (P.) et Cousot (R.). - Formal language, grammar and set-constraint-based program analysis by abstract interpretation. In : Proceedings of the 7 th ACM Conference on Functional Programming Languages and Computer Architecture. - La Jolla, Californie, juin 1995. À paraître.
[21]
Cridlig (R.) et Goubault (É.). - Semantics and analysis of Linda-based languages. In : Proceedings of the 3rd International Workshop WSA'93 on Static Analysis, éd. par Cousot (P.), Falaschi (M.), Filé (G.) et Rauzy (A.), pp. 72-86. - Springer-Verlag, Berlin, Allemagne, septembre 22-24, 1993.
[22]
Cridlig (R.). - An optimizing ML to C compiler. In : ACM SIGPLAN Workshop on ML and its Applications. pp. 28-36. - San Francisco, Californie, 20-21juin1992.
[23]
 *  Cridlig (R.). - Semantic analysis of shared-memory concurrent languages using abstract model-checking. In : Proceedings of the ACM Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM'95. - ACM Press, New York, U.S.A., juin 1995. À paraître.
[24]
Goubault (É.) et Jensen (T. P.). - Homology of higher dimensional automata. In : CONCUR'92, Proceedings of the Third International Conference on Concurrency Theory, éd. par Cleaveland (W. R.), pp. 254-268. - Springer-Verlag, Berlin, Allemagne, août 1992.
[25]
Goubault (É.). - Domains of higher-dimensional automata. In : CONCUR'93, Proceedings of the 4th International Conference on Concurrency Theory, éd. par Best (E.). pp. 293-307. - Springer-Verlag, Berlin, Allemagne, août 1993.
[26]
 *  Goubault (É.). - Schedulers as abstract interpretations of higher-dimensional automata. In : Proceedings of the ACM Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM'95. - ACM Press, New York, U.S.A., juin 1995. À paraître.
[27]
Granger (P.). - Static analysis of linear congruence equalities among variables of a program. In : TAPSOFT'91, Proceedings of the International Joint Conference on Theory and Practice of Software Development, éd. par Abramsky (S.) et Maibaum (T.S.E.), pp. 169-192. - Springer-Verlag, Berlin, Allemagne, 1991.
[28]
Granger (P.). - Improving the results of static analyses of programs by local decreasing iterations. In : Proceedings of the 12 th Foundations of Software Technology and Theoretical Computer Science Conference. pp. 68-79. - New Delhi, Inde, 18-20 décembre 1992, Lecture Notes in Computer Science 652, 1992.
[29]
Mauborgne (L.). - Abstract interpretation using TDGs. In : Proceedings of the Static Analysis Symposium, SAS'94, éd. par Le Charlier (B.), pp. 363-379,. - Springer-Verlag, Berlin, Allemagne, 1994.
[30]
Monsuez (B.). - Fractional types. BIGRE, Analyse Statique WSA'92, Bordeaux, IRISA, Rennes, France, vol. 81-82, 23-25 septembre 1992, pp. 274-284.
[31]
Monsuez (B.). - Polymorphic typing by abstract interpretation. In : Proceedings of the 12th Foundations of Software Technology and Theoretical Computer Science Conference. pp. 127-138. - New Delhi, Inde, 18-20 décembre 1992, Lecture Notes in Computer Science 652, 1992.
[32]
Monsuez (B.). - Polymorphic types and widening operators. In : Proceedings of the 3rd International Workshop WSA'93 on Static Analysis, éd. par Cousot (P.), Falaschi (M.), Filé (G.) et Rauzy (A.), pp. 267-281. - Springer-Verlag, Berlin, Allemagne, septembre 22-24, 1993.
[33]
Monsuez (B.). - Polymorphic typing for call-by-name semantics. In : Proceedings of the International Conference on Formal Methods in Programming and their Applications, éd. par rner (D. Bjø), Broy (M.) et Pottosin (I.V.), pp. 156-169. - Springer-Verlag, Berlin, Allemagne, juin 28-juillet 2, 1993.
[34]
 *  Monsuez (B.). - Using abstract insterpretation to define a strictness type inference system. In : Proceedings of the ACM Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM'95. - ACM Press, New York, U.S.A., juin 1995. À paraître.
Autres conférences
[35]
Cousot (P.) et Cousot (R.). - Comparison of the Galois connection and widening/narrowing approaches to abstract interpretation. JTASPEFL'91. BIGRE, vol. 74, octobre 1991, pp. 107-110.
[36]
Cousot (P.) et Cousot (R.). - Comparison of the Galois connection and widening/narrowing approaches to abstract interpretation, conférence invitée. In : ICLP'91 Pre-Conference Workshop on Semantics-based Analysis of Logic Programs. - Paris, France, 15 mai 1991.
[37]
Cousot (P.) et Cousot (R.). - Relational abstract interpretation of higher-order functional programs. JTASPEFL'91. BIGRE, vol. 74, octobre 1991, pp. 33-36.
[38]
Cousot (P.). - Constructing a hierarchy of semantics by abstract interpretation. In : Workshop on Logic, Domains and Programming Languages. - mai 24-27 1995.
[39]
Monsuez (B.). - An attempt to find polymorphic types by abstract interpretation. BIGRE, Actes JTASPEFL'91, Bordeaux, IRISA, Rennes, France, vol. 74, octobre 1991, pp. 18-26.
Thèses
[40]
Monsuez (B.). - Typage par Interprétation Abstraite. - Palaiseau, France, Thèse de doctorat de l'école polytechnique en informatique, École Polytechnique, 13 février 1994.
Notes de cours
[41]
Cousot (P.). - Algorithmique et programmation en Pascal (cours). - Ellipses, Paris, France, 1992, Cours de l'École Polytechnique. 297 p.
[42]
Cousot (P.). - Algorithmique et programmation en Pascal (exercices et corrigés). - Ellipses, Paris, France, 1992, Cours de l'École Polytechnique. 271 p.
[43]
Cousot (P.). - Calcul parallèle. - École Normale Supérieure, Notes de cours, M.M.F.A.I., mars 1995. 70 p.
[44]
Cousot (P.). - Langages de programmation et compilation. - École Normale Supérieure, Notes de cours, M.M.F.A.I., mars 1995. 133 p.
[45]
Cousot (P.). - Système d'exploitation Unix et réseaux d'ordinateurs et compilation. - École Polytechnique, Notes de cours, janvier 1995. 306 p.
Articles soumis ou en préparation
[46]
Goubault (É.). - Transitions take time. - LIENS, École Normale Supérieure, Paris, France, Soumis pour publication, 1995.
Rapports du DMI
[47]
Cousot (P.) et Cousot (R.). - Abstract Interpretation and Application to Logic Programs. - Rapport de recherche n'27 LIENS-92-12, École Normale Supérieure, Paris, France, Laboratoire d'Informatique, juin 1992.
[48]
Goubault (É.). - Higher Dimensional Automata, Part I - Basic Definitions. - Rapport de recherche. à paraître, École Normale Supérieure, Paris, France, Laboratoire d'Informatique, 1995.
Rapports de recherche publiés dans d'autres laboratoires
[49]
Cousot (P.) et Cousot (R.). - Forward and Backward Strictness Analysis by Abstract Interpretation of a Relational Semantics. - Rapport de recherche n'27 LIX/RR/94/05, École Polytechnique, Palaiseau, France, Laboratoire d'Informatique, février 1994.
[50]
Cousot (P.) et Cousot (R.). - Compositional and Inductive Semantical Definitions in Fixpoint, Equational, Constraint, Closure-condition, Rule-based and Game-Theoretic Form. - Rapport de recherche n'27 LIX/RR/95/01, École Polytechnique, France, Laboratoire d'Informatique, janvier 1995.
[51]
Cousot (P.) et Cousot (R.). - Formal Language, Grammar and Set-Constraint-Based Program Analysis by Abstract Interpretation. - Rapport de recherche n'27 LIX/RR/95/02, École Polytechnique, France, Laboratoire d'Informatique, janvier 1995.
[52]
   Cridlig (R.). - Un compilateur optimisant pour le langage ML. - Rapport d'option, Palaiseau France, École Polytechnique, juillet 1991.
[53]
Cridlig (R.). - Projection analysis by abstract interpretation. - Rapport de stage, École Polytechnique, École Normale Supérieure, Universités de Paris 6, 7 & 11, France, DEA "Informatique, Mathématiques et Applications", septembre 1992.
[54]
Goubault (É.). - Interprétation abstraite de systèmes de réécriture de graphes de termes. - Rapport de stage, École Polytechnique, École Normale Supérieure, Universités de Paris 6, 7 & 11, France, DEA "Informatique, Mathématiques et Applications", 11 septembre 1991.
[55]
Mauborgne (L.). - Abstract interpretation using TDGs. - Rapport de stage, École Polytechnique, École Normale Supérieure, Universités de Paris 6, 7 & 11, France, DEA "Informatique, Mathématiques et Applications", septembre 1993.
[56]
Védrine (F.). - Galois connection based abstract interpretation for binding time analysis. - Rapport de stage, École Polytechnique, École Normale Supérieure, Universités de Paris 6, 7 & 11, France, DEA "Informatique, Mathématiques et Applications", 13 juillet 1994.
Brevets
[57]
Goubault (É.). - A vector quantizing method for coding signals and system for implementing said method. - Premier inventeur du brevet européen numéro 91480054.5 déposé pour IBM France, puis breveté aux États-Unis, 29 mars 1991.
[58]
Goubault (É.). - Improved method for coding digital data using vector quantizing techniques and device for implementing said method'. - Premier inventeur du brevet européen numéro 92480097.2 déposé pour IBM France., 30 juin 1992.



File translated from TEX by TTH, version 3.59.
On 6 Nov 2004, 10:05.