Département d'Informatique de l'École Normale Supérieure
Rapport scientifique de l'équipe
Interprétation abstraite et sémantique



(1998-2001)











Membres de l'équipe

Activité scientifique de l'équipe

1   Interprétation abstraite

L'interprétation abstraite est une théorie de l'approximation des structures mathématiques intervenant dans la définition de la sémantique des langages informatiques, qu'il s'agisse de langages de programmation ou de langages de spécification de ces systèmes informatiques. Diverses introductions sont proposées dans [5, 6, 7].

2   Conception de hiérarchies de sémantiques par interprétation abstraite

La sémantique d'un programme spécifie formellement les comportements possibles d'un système informatique exécutant ce programme en interaction avec un environnement quelconque. L'interprétation abstraite offre un point de vue constructif et unificateur sur les sémantiques des langages de programmation. En effet, en faisant varier le niveau d'observation de ces comportements à l'exécution, qui peut être plus ou moins précis, l'interprétation abstraite permet de construire des hiérarchies de sémantiques intégrant toutes les sortes de sémantiques existantes ainsi que de nouvelles variantes [12, 11]. La conception de hiérarchies de sémantiques pour des familles de langages de programmation sert de fondements pour concevoir une grande variété d'analyseurs statiques pour ces langages.

3   Analyse statique par interprétation abstraite

L'application la plus connue de l'interprétation abstraite est l'analyse statique [9]. Si l'approximation est suffisamment grossière, l'abstraction d'une sémantique peut permettre d'en donner une version moins précise mais calculable par l'ordinateur. De ce fait un ordinateur est capable d'analyser le comportement de programmes et de logiciels avant même de les exécuter. La perte d'information ne permet pas de répondre à toutes les questions relatives à la sémantique concrète, mais toutes les réponses données par calcul effectif de la sémantique abstraite sont toujours justes. Les applications de l'analyse statique concernent la compilation optimisante et la transformation de programmes mais principalement la mise au point et la vérification des conditions de bon fonctionnement des systèmes informatiques (comme les systèmes critiques embarqués pour le contrat européen DAEDALUS).

4   Algèbres de propriétés abstraites

Il est encore et toujours nécessaire d'étendre la gamme des analyses disponibles pour permettre de choisir le meilleur compromis entre la précision de l'analyse et son coût, en particulier pour analyser de très grands programmes (de plusieurs centaines de milliers à quelques millions de lignes). Par conséquent, une activité essentielle de l'équipe sur l'analyse statique concerne la recherche de nouvelles approximations de classes de propriétés de programmes qui soient à la fois expressives et performantes.

Cette idée se formalise par des algèbres abstraites utilisées pour définir des sémantiques approchées de langages de programmation dont le calcul effectif permet de déterminer automatiquement et statiquement les propriétés dynamiques d'un programme.

Une algèbre abstraite comprend d'une part un domaine abstrait dont les éléments représentent les propriétés abstraites considérées par l'analyse. D'autre part, une algèbre abstraite comprend des opérations abstraites qui formalisent la sémantique abstraite des principales primitives des langages de programmation (par exemple des approximations de transformateurs de prédicats). L'étude mathématique de la correspondance entre les algèbres de propriétés abstraites et la sémantique concrète doit être complétée par la conception de structures de données et d'opérations informatiques conduisant à une implantation en machine efficace. Ces algèbres abstraites peuvent être développées et étudiées indépendamment des langages de programmation et des analyses particulières.

Cette étude des algèbres de propriétés abstraites est particulièrement importante pour l'application pratique de l'interprétation abstraite, puisque le domaine abstrait et les structures de données utilisées pour représenter ses éléments vont déterminer à la fois la précision et la complexité des analyses. Pour une plus grande précision, les structures de données pour les domaines abstraits doivent permettre de représenter autant d'objets que possibles, et pour une meilleure complexité, ils doivent permettre de calculer efficacement les opérations abstraites associées, deux objectifs difficilement conciliables. D'autre part, les analyses les plus fines utilisent en général la possibilité d'approximer certains de ces calculs de manière dynamique à l'aide d'opérateurs d'élargissement. Ces élargissements doivent donc aussi être facilités par les structures de données des domaines abstraits.

Nous étudions également la façon de construire ces algèbres par composition d'algèbres plus simples. D'un point de vue informatique les algèbres abstraites s'implantent comme des modules et des foncteurs fournis à des analyseurs statiques génériques permettant de mettre en oeuvre de nombreuses analyses et donc de réaliser de nombreuses expérimentations.

5   Algèbres de propriétés abstraites symboliques

Il s'agit de représenter des propriétés et donc des ensembles infinis d'objets informatiques symboliques (par exemple séquences, listes, arbres, graphes) eux-mêmes généralement infinis (puisqu'il faut bien prendre en compte le cas des programmes dont l'exécution ne termine pas).

En général, les structures de données classiques disponibles ne sont pas bien adaptées, et ce pour deux raisons : d'une part les opérations abstraites ne sont pas forcément celles pour lesquelles les représentations sont les plus efficaces, d'autre part les possibilités d'approximation et plus encore d'élargissement ne sont en général pas offertes. Il faut donc soit adapter les structures de données existantes en inventant des élargissements compatibles, soit inventer de nouvelles structures de données. Cette dernière voie permet d'utiliser, dès la conception des structures de données, les possibilités d'approximations sûres offertes par le cadre de l'interprétation abstraite.

5.1   Relations entre ensembles finis

Les analyses précises doivent tenir compte des liens entre les propriétés de différentes parties des programmes. Par exemple, on peut vouloir représenter les relations entre les propriétés d'entrée et celles de sortie pour fournir une analyse modulaire. Si les propriétés des différentes parties des programmes peuvent être finies, on peut utiliser des relations entre ensembles finis pour coder les liens entre les propriétés. L'avantage de cette approche est qu'il existe une manière classique et efficace de les représenter, à condition que le nombre d'ensembles à relier soit lui-même fini. Il s'agit des diagrammes de décision binaires (« Binary Decision Diagrams », BDDs), qui partagent autant que possible les sous-relations isomorphes. Ces représentations peuvent être adaptées à la représentation de fonctions d'ordre supérieur, et il est possible de définir des opérateurs d'élargissement basés sur leur taille. Ces extensions ont été appliquées avec succès à l'analyse de nécessité [15].

Lorsque les propriétés à analyser sont plus fines, comme les propriétés de terminaison ou les propriétés temporelles comme l'équité, il est nécessaire de relier un nombre infini d'ensembles. On peut dans ce cas utiliser une autre représentation classique, les automates de Büchi, mais leur complexité est trop grande vis-à-vis des opérations abstraites. Nous proposons donc une extension des BDDs, les graphes de décisions [29], qui gardent les propriétés de partage des BDDs. Les graphes de décision sont plus efficaces que les automates de Büchi, au prix d'une légère perte d'expressivité. Cette nouvelle représentation permet d'exprimer des propriétés de vivacité ou d'équité, mais impose d'approximer les unions de relations.

5.2   Ensembles d'arbres

Les langages d'arbres permettent d'exprimer les propriétés les plus complexes, surtout lorsqu'ils contiennent des arbres infinis. On peut par exemple facilement exprimer des propriétés de traces d'exécutions concurrentes, de sécurité de protocoles crytpographiques ou encore d'état de la mémoire en cours d'exécution. Encore une fois, les représentations classiques, que ce soit par automates ou grammaires, ne sont pas adaptées à l'analyse de programmes.

Nous proposons une nouvelle représentation, fondée sur une décomposition canonique des ensembles d'arbres. Cette décomposition extrait d'une part la forme arborescente de l'ensemble, par un partage préfixe maximum, et d'autre part des relations entre les sous-arbres de cette forme arborescente [43]. La forme arborescente peut être représentée de manière très efficace par des squelettes d'arbres [30], qui partagent aussi naturellement les sous-arbres et ensembles de sous-arbres communs. Ces squelettes constituent une première approximation des propriétés, facile à manipuler et structurellement proche des ensembles d'arbres, ce qui facilite la mise au point d'opérateurs d'élargissement.

Ces représentations sont ensuite raffinées à l'aide de relations pour former des schémas d'arbres [31]. Le pouvoir expressif et la complexité de ces structures dépend du type de représentation utilisée pour les relations. En utilisant des relations finies, on peut déjà exprimer des langages hors de portée des automates classiques, comme {anbncn| n³ 0}. Avec les graphes de décision décrits plus haut, on peut facilement exprimer des preuves de terminaison sous hypothèse d'équité. La validation pratique de ces techniques devrait pouvoir être obtenue grâce à leur application dans le cadre du contrat européen DAEDALUS.

6   Algèbres de propriétés abstraites numériques

La majeure partie des programmes informatiques manipulent des variables numériques entières ou à virgule flottante. L'analyse des valeurs prises par ces variables est très importante car elle permet à elle seule de découvrir plusieurs types de bogues très répandus, comme les dépassements de tableau, les divisions par zéro ou les boucles infinies. On utilise pour cela des domaines numériques abstraits. Actuellement, parmi les domaines numériques abstraits existants et utilisés, on cite : le domaine des intervalles, peu coûteux (coût linéaire) mais peu précis, et le domaine des polyèdres plus précis mais très coûteux (coût exponentiel).

Dans le but d'améliorer la granularité des analyses numériques, nous avons développé deux nouveaux domaines numériques abstraits : le domaine des différences bornées [32] et le domaine des octogones [61]. Ces domaines sont basés d'une part sur une structure de données qui a déjà fait ses preuves dans le domaine de la vérification de modèles (« model--checking ») : les « Difference--Bound Matrices » (DBMs) et d'autre part sur l'algorithmique des graphes pondérés. Le coût (coût cubique en temps et quadratique en mémoire) et la précision de ces domaines est intermédiaire entre ceux du domaine des intervalles et ceux des polyèdres. Un point important à noter est que ces domaines sont relationnels, c'est--à--dire aptes à capturer des relations numériques entre plusieurs variables, ce qui n'est pas le cas du domaine des intervalles.

En pratique, ces domaines abstraits se sont révélés un bon compromis et ils ont permis des analyses hors de portée du domaine des intervalles pour un coût beaucoup plus faible que le domaine des polyèdres.

7   Analyses statiques de systèmes mobiles

De vastes réseaux de communications sont utilisés pour répondre aux besoins de notre société. Ces derniers permettent de concevoir des systèmes de processus distants, dans lesquels plusieurs processus sont exécutés en différents sites d'un réseau et interagissent en communiquant. De nouveaux processus peuvent être créés dynamiquement. De plus, ce qui est plus récent, la distribution des processus peut varier au cours du temps : c'est la programmation mobile.

Il est très difficile de prouver que le comportement d'un très gros programme est conforme à une spécification donnée. C'est encore plus délicat dans le cadre de la programmation mobile. Pourtant, nous nous devons de montrer que les systèmes mobiles que nous utilisons sont sûrs. Ainsi, dans le cadre de la téléphonie mobile, une société qui utilise un réseau de processus mobiles doit être sûre que son réseau ne demandera pas d'utiliser plus de ressources qu'elle ne peut en fournir et que les contraintes de confidentialité sur les informations qui circulent sur ce réseau ne peuvent pas être violées.

7.1   Modèles du code mobile

Avant tout, nous avons besoin d'un modèle pour décrire la mobilité et nous permettre d'isoler et de mieux comprendre les problèmes qui lui sont liés. Ces modèles servent ensuite de base à la conception de langages de haut niveau utilisables en pratique. Plusieurs modèles de la mobilité ont été proposés. Le p-calcul de Milner code implicitement la mobilité. Il met en jeu des systèmes de processus qui interagissent en échangeant des noms de canaux. Ces interactions permettent non seulement de synchroniser l'exécution des processus, mais aussi de changer dynamiquement la distribution de ces processus. Le p-calcul est à la base du langage Erlang que la société Ericson a utilisé pour développer des réseaux de téléphonie mobile. Le modèle des ambients mobiles code explicitement la mobilité. Il représente à la fois la structure hiérarchique des sites administratifs d'un réseau, et la répartition des processus sur ces sites. En interagissant, les processus peuvent déplacer les sites dans lesquels ils sont exécutés.

7.2   Analyses statiques de code mobile

Plusieurs analyses ont été proposées pour garantir ou prouver des propriétés sur les systèmes mobiles. Elles considèrent essentiellement des propriétés de sûreté (« safety properties »), comme la confidentialité de l'information qui circule dans les systèmes de communication ou le nombre de processus qui sont utilisés par les systèmes. Elles consistent essentiellement à montrer que les configurations qui conduiraient à la perte de la propriété que nous cherchons à valider n'apparaissent jamais.

Nous distinguons deux types de propriétés qui suffisent à garantir l'absence de telles configurations :

L'étude des systèmes mobiles est un enjeu important. Jusqu'à maintenant, toutes les analyses ont essentiellement porté sur des propriétés de sûreté et ne sont efficaces que sur des petits exemples. Il est indispensable de prendre en compte les propriétés de vivacité et de proposer des méthodes pour leur analyse. Il est important de passer à l'échelle industrielle et de considérer l'étude des langages réels comme Erlang. Ceci ne peut être fait sans une analyse modulaire des réseaux, qui permette non seulement d'analyser un système morceau par morceau, mais aussi de regrouper l'information obtenue.

8   Analyses statiques probabilistes

Il est parfois nécessaire de considérer des programmes au comportement probabiliste, que ce soit pour l'étude des algorithmes probabilistes proprement dits ou pour l'étude de systèmes embarqués placés dans un environnement décrit de façon probabiliste. Dans ce dernier cas, il est en particulier intéressant d'estimer la probabilité d'atteindre des états de panne ou la probabilité que le temps d'exécution dépasse un certain seuil. Nous avons donc recherché des méthodes permettant d'obtenir par interprétation abstraite de telles estimations, ou du moins des majorants sur les valeurs considérées.

Ces recherches ont été menées avec deux objectifs : Afin de pouvoir garantir l'exactitude mathématique des analyses, nous avons dû définir des sémantiques adaptées aux programmes probabilistes et donner des relations d'abstraction ou d'équivalence entre elles. Parmi les sémantiques possibles, certaines donnent directement des possibilités d'analyse par interprétation abstraite: Nous avons développé des treillis abstraits adaptés à ces sémantiques : Ces méthodes souffrent néanmoins d'une certaine complexité, aussi nous avons développé une méthode d'implantation plus simple, combinant interprétation abstraite et statistiques de Monte-Carlo [36, 63]. Cette méthode fournit des bornes supérieures d'évènements rares ainsi qu'une probabilité que cette borne soit valable. Une analyse préalable par interprétation abstraite ordinaire permet de limiter le nombre d'échantillons nécessaires à une bonne estimation. L'analyse est parallélisable avec un gain linéaire et peu de communications, ce qui permet de l'implanter sur un réseau de PC, peu coûteux par rapport à une machine parallèle conventionnelle. Cette méthode étant assez simplement adaptable à un analyseur préexistant, le CEA doit prochainement l'implanter dans son analyseur industriel Caveat.

Nous avons en outre développé un petit analyseur prototype de démonstration pour deux de nos analyses [33, 36].

9   Analyses statiques temporelles

Les analyses statiques classiques portent essentiellement sur les propriétés de sûreté (« safety ») ou d'invariance (comme l'absence d'erreurs à l'exécution). Au delà des propriétés de sûreté, il est maintenant fréquent de vouloir vérifier automatiquement des propriétés de programmes plus fines et donc, en général, également beaucoup plus complexes comme les propriétés temporelles [27]. L'exemple le plus connu de propriété temporelle est la vivacité (« liveness »), par exemple pour démontrer automatiquement la terminaison de processus parallèles équitables partageant des données communes [31].

10   Analyses statiques et vérification de modèles (« model checking »)

La vérification de modèles a pour limite l'hypothèse de finitude, voire la complexité pratique notamment en mémoire. L'abstraction, c'est-à-dire l'approximation par interprétation abstraite, est donc nécessaire pour la vérification de modèles infinis.

Nous avons étudié la limite des tendances actuelles de la recherche visant à automatiser l'abstraction interactivement en montrant pour les spécifications de sûreté que la découverte de l'abstraction et la preuve de la correction de l'abstraction sont logiquement équivalentes à une preuve formelle de correction de la spécification [8, 17].

Une autre tendance de la recherche en vérification de modèles est l'abstraction d'un système de transition concret par un système de transition abstrait de manière à pouvoir réutiliser les vérificateurs de modèles existants. Nous avons proposé une autre façon de procéder consistant à effectuer en parallèle une analyse statique abstraite et la vérification de modèle concret, de manière à réduire l'espace des états à explorer tout en utilisant une plus grande variété d'abstractions non forcément réduites à des systèmes de transition abstraits [13].

11   Réalisation mécanisée d'interpréteurs abstraits

Un interpréteur abstrait doit fournir un résultat sûr ; mais peut-on faire confiance à l'analyse proposée et à son implantation ? Nous avons étudié la possibilité de formaliser dans un environnement de preuve assistée par ordinateur (Coq) la correction d'un interpréteur abstrait telle qu'elle est définie par la théorie de l'interprétation abstraite. Cette correction est notamment assurée par l'usage de modules paramétriques prouvés corrects selon la spécification de leurs paramètres. En instanciant ces modules, il est possible de produire automatiquement un interpréteur abstrait certifié. Nous avons illustré cela par la production d'un petit interpréteur certifié [47].

12   Applications de l'analyse statique par interprétation abstraite

12.1   Analyse statique de protocoles cryptographiques

L'étude des protocoles cryptographiques (commerce électronique, authentification pour l'accès à un système informatique) peut se faire à deux niveau : au niveau des primitives cryptographiques ou au niveau de la correction du protocole lui-même, les primitives étant supposées vérifier certaines propriétés. Nous nous sommes intéressés à ce second aspect des choses.

Supposant idéales les primitives cryptographiques, nous exprimons les protocoles dans le modèle de Dolev-Yao, où les données échangées sont des termes sur une signature décrivant les primitives utilisées et les constantes générées. Il est alors possible de définir une sémantique des protocoles modélisant le cas d'un intrus contrôlant le réseau. S'il n'est alors évidemment pas possible dans un modèle où l'intrus a un pouvoir aussi grand de démontrer des propriétés de vivacité, il est néanmoins possible de s'assurer de la sécurité du protocole : certaines données secrètes ne doivent en aucun cas tomber en la possession de l'intrus, ou certaines machines ne doivent pas parvenir à un état marquant le bon fonctionnement tout en ayant accepté certaines données incorrectes.

Nous approchons cette sémantique par interprétation abstraite en utilisant un domaine d'automates d'arbres [33, 64]. Cette analyse a été implantée dans un prototype.

12.2   Test abstrait de logiciel

Les sociétés modernes sont très informatisées et donc hautement sensibles aux bogues dans les logiciels, en particulier ceux qui pilotent des systèmes critiques que l'on trouve dans les transports, la médecine ou le commerce électronique. Les travaux sur la vérification des logiciels sont donc très nombreux et la fiabilité et la sûreté de fonctionnement du logiciel constitue certainement une des applications principales de l'analyse statique de programmes. Cependant, toutes les méthodes automatiques de vérification de logiciels ont des limites théoriques liées aux problèmes d'indécidabilité (ce qui implique ultimement une intervention humaine) et des limites pratiques dues aux difficultés d'usage. De ce fait, le test est encore la méthode la plus utilisée pour mettre au point les programmes industriels.

Le test abstrait [10] repose sur l'idée de vérifier la correction des programmes par morceaux sur des spécifications partielles, mais en remplaçant les jeux de données par des spécifications fournies sous forme de propriétés abstraites spécifiant les comportements souhaités des programmes. Les exécutions sur ces jeux de données sont alors remplacées par des analyses statiques.

Le test abstrait étant facilement compréhensible par analogie avec les méthodes de test classiques, on peut espérer qu'il n'y aura pas de difficultés d'usage. L'intervention humaine, ultimement nécessaire, est limitée à la compréhension des algèbres abstraites utilisées à des niveaux de raffinement variés. On peut donc espérer un excellent taux de couverture pour un coût humain raisonnable, même pour de grands programmes.

12.3   Tatouage de logiciels par interprétation abstraite

Parmi les applications originales de l'analyse statique par interprétation abstraite, citons le tatouage de code mobile permettent au propriétaire d'incruster dans le code source de manière indécelable et indélébile une greffe logicielle identifiant ce composant [58]. La marque indélébile à inclure n'est pas inscrite directement dans le texte du programme, ce qui la rendrait trop facilement modifiable, mais dans le comportement à l'exécution de l'objet sans que cela altère ses fonctionnalités d'origine. Ces informations sont invisibles lors de l'utilisation de l'objet mais peuvent être extraites par analyse statique.

13   Perspectives

L'équipe travaille sur le thème de l'efficacité et de la fiabilité des systèmes informatiques qui est porteur au delà des évolutions rapides de l'informatique et vertical depuis la théorie jusqu'à, plus récemment, l'industrialisation d'abord aux USA puis en Europe. L'équipe a une visibilité internationale que traduisent les invitations, les visiteurs et les contrats. Elle participe au transfert technologique (au travers de l'essaimage des doctorants et par les contrats impliquant des industriels).

L'équipe est petite (avec deux enseignants permanents dont un depuis septembre 2000 et trois doctorants), avec un grand taux de renouvellement. L'équipe a donc des possibilités de croissance, ce qui est nécessaire pour répondre aux problèmes et satisfaire aux besoins de formation par la recherche résultant de la phase actuelle d'industrialisation de l'interprétation abstraite.

Eléments d'évaluation

1   Collaborations

2   Missions, conférences et séminaires

3   Accueil de chercheurs

4   Diffusion de la connaissance

5   Réalisation et diffusion de logiciels, brevets

La taille de l'équipe ne permet pas de développer des analyseurs statiques de qualité industrielle (dont le coût de développement est souvent supérieur à 25 personnes/années) et d'assurer ensuite leur maintenance et le suivi de leur évolution. Par conséquent, les logiciels développés dans l'équipe sont des prototypes dont le coût de développement est de l'ordre de quelques personnes/mois (en général 3 à 9 personnes/mois). Ces prototypes servent essentiellement à l'expérimentation nécessaire pour estimer le coût et la précision des analyses.

6   Participation à l'évaluation de la recherche

7   Encadrement doctoral

8   Enseignement

9   Prix et distinctions

Patrick Cousot a reçu la médaille d'argent du CNRS en 2000.

Publications



Édition d'actes ou d'ouvrages collectifs
[1]
P. Cousot (éditeur). -- Proc. 8th International Static Analysis Symposium SAS '01. -- Springer--Verlag, juillet 2001, Lecture Notes in Computer Science. À paraître.

[2]
P. Cousot, É. Goubault, J. Gunawardena, M. Herlihy, M. Raussen et V. Sassone (éditeurs). -- GEometry and Topology in COncurrency theory. -- Elsevier, 2001, volume 39. http://www.elsevier.nl/locate/entcs/volume39.html.

Chapitres de livres ou d'ouvrages collectifs
[3]
P. Cousot. -- The calculational design of a generic abstract interpreter. In : Calculational System Design, éd. par M. Broy et R. Steinbrüggen, pp. 421--505. -- NATO Science Series, Series F: Computer and Systems Sciences. IOS Press, 1999, volume 173.

[4]
P. Cousot. -- Abstract interpretation based formal methods and future challenges, papier invité. In : « Informatics --- 10 Years Back, 10 Years Ahead », éd. par R. Wilhelm, pp. 138--156. -- Sarrebruck, DE, Springer--Verlag, 28--31 août 2000, Lecture Notes in Computer Science, vol. 2000.

Articles invités
[5]
P. Cousot. -- Directions for research in approximate system analysis, papier invité. ACM Comput. Surv., vol. 31, n° 3es, septembre 1999.

[6]
P. Cousot. -- Abstract interpretation: Achievements and perspectives, papier invité. Proc. SSGRR 2000 -- Advances in Infrastructure for Electronic Business, Science, and Education on the Internet, 31 juillet -- 6 août 2000.

[7]
P. Cousot. -- Interprétation abstraite, papier invité. TSI, vol. 19, n° 1-2-3, janvier 2000, pp. 155--164.

[8]
P. Cousot. -- Partial completeness of abstract fixpoint checking, papier invité. Proc. 4th International Symposium on Abstraction, Reformulation and Approximation, SARA '00. Lecture Notes in Artificial Intelligence, vol. 1864, 26--29 juillet 2000, pp. 1--25. -- Horseshoe Bay, TX, USA.

[9]
P. Cousot. -- Abstract interpretation based static analysis parameterized by semantics, papier invité. Proc. 4th International Static Analysis Symposium, SAS '97. Lecture Notes in Computer Science, vol. 1302, 8--10 septembre 1997, pp. 388--394.

[10]
P. Cousot et R. Cousot. -- Abstract interpretation based program testing, papier invité. Proc. SSGRR 2000 -- Advances in Infrastructure for Electronic Business, Science, and Education on the Internet, 31 juillet -- 6 août 2000.

Articles dans des revues internationales avec comité de lecture
[11]
P. Cousot. -- Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theoret. Comput. Sci., À paraître en 2001 (Version préliminaire dans [12]).

[12]
P. Cousot. -- Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Electronic Notes in Theoretical Computer Science, ENTCS, vol. 6, 1997. -- http://www.elsevier.nl/locate/entcs/volume6.html, 25 pages.

[13]
P. Cousot et R. Cousot. -- Refining model checking by abstract interpretation. Automated Software Engineering Journal, special issue on Automated Software Analysis, vol. 6, 1999, pp. 69--95.

[14]
J. Feret. -- Occurrence counting analysis for the p-calculus. Electronic Notes in Theoretical Computer Science, ENTCS, vol. 39, 2001.

[15]
L. Mauborgne. -- Abstract interpretation using typed decision graphs. Science of Computer Programming, vol. 31, n° 1, mai 1998, pp. 91--112.

[16]
L. Mauborgne. -- An incremental unique representation for regular trees. Nordic Journal of Computing, vol. 7, n° 4, 2000, pp. 290--311.

Conférences invitées
[17]
P. Cousot. -- On completeness in abstract model checking from the viewpoint of abstract interpretation, conférence invitée. In : Réunion Workshop on Implementation of Logics, Saint Gilles, La Réunion. -- 11--12 novembre 2000.

[18]
P. Cousot. -- Abstract interpretation and types, conférence invitée. In : Workshop on « Static Analysis and Types », Palazzo del Bó, Padoue, IT. -- 17--18 mai 1999.

[19]
P. Cousot. -- Discrete fixpoint approximation methods in program static analysis, conférence invitée. In : 7th Int. Coll. on Numerical Analysis and Computer Science with Applications, NACSA '98, Plovdiv, BG, 13--17 août 1998.

[20]
P. Cousot. -- Rule-based specifications and their abstract interpretation, conférence invitée. In : 4th Advanced Seminar on Foundations of Declarative Programming, ASFDP '98. -- 15 juin 1998. Valence, Espagne.

[21]
P. Cousot. -- Abstraction in abstract interpretation, conférence invitée. In : Workshop on Refinement and Abstraction, ETL, Osaka, Japon. -- 15--17 novembre 1999.

[22]
P. Cousot. -- An overview of abstract interpretation and program static analysis, conférence invitée. In : 1st Int. Advisory Board Workshop, EECS Dept., KAIST, Taeduk Science Complex, Taejon, République de Corée. -- 14 juin 2000.

[23]
P. Cousot. -- Progress on abstract interpretation based formal methods and future challenges, conférence invitée. In : Conference at the Occasion of Dagstuhl's 10th Anniversary, « Informatics --- 10 Years Back, 10 Years Ahead », Saarland University Campus, Sarrebruck, DE. -- 28--31 août 2000.

[24]
P. Cousot. -- Abstract interpretation for software verification, conférence invitée. In : Workshop on Formal Design of Safety Critical Embedded Systems, FEmSys '2001, Munich, DE. -- 21--23 mars 2001.

[25]
P. Cousot et R. Cousot. -- Abstract testing versus abstract model-checking, conférence invitée. In : Schloß Ringberg Seminar on « Model Checking and Program Analysis », organisé par A. Podelski, B. Steffen et M. Vardi. -- 20--23 février 2000.

Communications dans des conférences internationales avec comité de lecture
[26]
P. Cousot et R. Cousot. -- Abstract interpretation of algebraic polynomial systems. In : Proc. 6th International Conference on Algebraic Methodology and Software Technology, AMAST '97, éd. par M. Johnson. Lecture Notes in Computer Science, vol. 1349, pp. 138--154. -- Springer--Verlag, 13--18 décembre 1997. Sydney, AU.

[27]
P. Cousot et R. Cousot. -- Temporal abstract interpretation. In : Conference Record of the 27th Annual ACM SIGPLAN-SIGACT Symposium on Principles of programming Languages, POPL '00, Boston, MA, janvier 2000. pp. 12--25. -- ACM Press.

[28]
J. Feret. -- Confidentiality analysis of mobile systems. In : Proc. 7th International Static Analysis Symposium, SAS '00. Lecture Notes in Computer Science, vol. 1824, pp. 135--154. -- Springer--Verlag, 2000.

[29]
L. Mauborgne. -- Binary decision graphs. In : Proc. 6th International Static Analysis Symposium SAS '99, éd. par A. Cortesi et G. Filé. Lecture Notes in Computer Science, vol. 1694, pp. 101--116. -- Springer--Verlag, 1999.

[30]
L. Mauborgne. -- Improving the representation of infinite trees to deal with sets of trees. In : European Symposium on Programming, ESOP 2000, éd. par G. Smolka. Lecture Notes in Computer Science, vol. 1782, pp. 275--289. -- Springer--Verlag, 2000.

[31]
L. Mauborgne. -- Tree schemata and fair termination. In : Proc. 7th International Static Analysis Symposium SAS '00, éd. par J. Palsberg. Lecture Notes in Computer Science, vol. 1824, pp. 302--320. -- Springer--Verlag, 2000.

[32]
A. Miné. -- A new numerical abstract domain based on difference-bound matrices. In : 2nd Symposium on Programs as Data Objects, Lecture Notes in Computer Science. -- 2001. À paraître.

[33]
D. Monniaux. -- Abstracting cryptographic protocols with tree automata. In : 6th International Static Analysis Symposium, SAS '99. Lecture Notes in Computer Science, n°1694, pp. 149--163. -- Springer--Verlag, 1999.

[34]
D. Monniaux. -- Decision procedures for the analysis of cryptographic protocols by logics of belief. In : 12th Computer Security Foundations Workshop. -- IEEE, 1999.

[35]
D. Monniaux. -- Abstract interpretation of probabilistic semantics. In : 7th International Static Analysis Symposium, SAS '00. Lecture Notes in Computer Science, n°1824, pp. 322--339. -- Springer--Verlag, 2000.

[36]
D. Monniaux. -- An abstract Monte-Carlo method for the analysis of probabilistic programs (extended abstract). In : Conference Record of the 28th Annual ACM SIGPLAN-SIGACT Symposium on Principles of programming Languages, POPL '01). pp. 93--101. -- ACM Press, 2001.

[37]
D. Monniaux. -- Backwards abstract interpretation of probabilistic programs. In : European Symposium on Programming. Lecture Notes in Computer Science. -- Springer--Verlag, 2001.

Autres conférences
[38]
P. Cousot. -- A few remarks on the abstraction and equivalence of semantics. In : IFIP WG 2.3, Obernai. -- 26 septembre 1997.

[39]
P. Cousot. -- Introduction to a discussion on mechanical formal methods for software verification. In : IFIP WG 2.3 Santa Cruz Meeting. -- 7--12 janvier 2001.

Thèses et habilitations
[40]
B. Blanchet. -- Analyse d'échappement, Applications à ML et JavaTM. -- Thèse de doctorat en informatique, École polytechnique, 7 décembre 2000.

[41]
L. Correnson. -- Sémantique équationelle. -- Thèse de doctorat en informatique, École polytechnique, 1er avril 2000.

[42]
J. Goubault. -- Logique, complexité, démonstration automatique et thèmes connexes. -- Habilitation à diriger les recherches, Université de Paris 9, Dauphine, 27 juin 1997.

[43]
L. Mauborgne. -- Représentation d'ensembles d'arbres pour l'interprétation abstraite. -- Thèse de doctorat en informatique, École polytechnique, 25 novembre 1999.

[44]
F. Védrine. -- Analyses totales de programmes par l'interprétation abstraite. -- Thèse de doctorat en informatique, École polytechnique, 28 janvier 2000.

Rapports de DEA
[45]
D. Massé. -- Interprétation abstraite du langage de programmation LUSTRE. -- Mémoire de stage de DEA programmation : sémantique, preuves et langages, ENS, 1998.

[46]
A. Miné. -- Représentation d'ensembles de contraintes de somme ou de différence de deux variables et application à l'analyse automatique de programmes. -- Mémoire de stage de DEA programmation : sémantique, preuves et langages, ENS, 2000. http://www.eleves.ens.fr:8080/home/mine/stage_dea/index.shtml.en.

[47]
D. Monniaux. -- Réalisation mécanisée d'interpréteurs abstraits. -- Rapport de DEA programmation : sémantique, preuves et langages, Université Paris VII, 1998.

Notes de cours
[48]
P. Cousot. -- Workshop on abstract interpretation. -- 10--15 novembre 1997. KAIST, Taeduk Science Complex, Taejon, KR.

[49]
P. Cousot. -- Calculational design of semantics and static analyzers by abstract interpretation. -- 28 juillet -- 9 août 1998. NATO Int. Summer School 1998 on Calculational System Design. Marktoberdorf, DE. Organized by F.L. Bauer, M. Broy, E.W. Dijkstra, D. Gries and C.A.R. Hoare.

[50]
P. Cousot. -- Corso di interpretazione astratta. -- 9--12 septembre 1998. Dottorato di Ricerca, Dip. di Informatica, Univ. di Udine, IT.

[51]
P. Cousot. -- Interprétation abstraite. -- 1er avril 1998. École jeunes chercheurs en programmation, GDR Programmation du CNRS, École des Mines de Nantes, Nantes, 23 mars -- 2 avr. 1998.

[52]
P. Cousot. -- Analyse statique de logiciels : du test exhaustif à la vérification automatique. -- 28 janvier 1999. Séminaire de formation de l'Institut de l'École normale supérieure et du Collège de Polytechnique sur l'« Analyse Statique de Logiciels », Paris.

[53]
P. Cousot. -- Interprétation abstraite. -- 24--25 octobre 2000. Journées ASPROM sur la Sûreté des Logiciels, Paris.

[54]
P. Cousot. -- Langage de programmation et compilation. -- 10 octobre 2000. Magistère MMFAI.

[55]
P. Cousot. -- Sémantique des langages de programmation. -- 10 octobre 2000. Magistère MMFAI.

[56]
P. Cousot et R. Cousot. -- Introduction to abstract interpretation. -- 28 juillet -- 9 août 1998. Course notes for the « NATO International Summer School 1998 on Calculational System Design », Marktoberdorff, DE.

[57]
L. Mauborgne. -- Sets of trees and abstract interpretation. -- février -- mars 2000. Cours à l'Université de Copenhague.

Brevets
[58]
P. Cousot, R. Cousot, M. Riguidel et A. Venet. -- Dispositif et procédé pour la signature, le marquage et l'authentification de programmes logiciels ou matériels d'ordinateur. -- Brevet en cours de dépôt.

Articles soumis ou en préparation
[59]
J. Feret. -- Abstract interpretation-based static analysis of mobile ambients. -- Soumis à SAS '01.

[60]
J. Feret. -- Dependency analysis of mobile systems. -- Soumis à CAV '01.

[61]
A. Miné. -- The octagon abstract domain, 2001. Soumis à SAS '01.

[62]
D. Monniaux. -- An abstract analysis of the probabilistic termination of programs. -- 2001. Soumission à SAS '01.

[63]
D. Monniaux. -- An abstract Monte-Carlo method for the analysis of probabilistic programs. -- 2001. En préparation pour soumission au journal ACM TOPLAS.

[64]
D. Monniaux. -- Abstracting cryptographic protocols with tree automata. -- 2001. Version étendue de [33]. En cours de soumission à Science of Computer Programming.

Miscellanea
[65]
P. Cousot. -- Contribution to the panel on « Abstractions in AI and software engineering ». -- 4th Int. Symp. SARA '2000, Horseshoe Bay, TX, USA, 26--29 juil. 2000.

[66]
P. Cousot. -- Research on abstract interpretation at ENS with a few words on software abstract watermarking. -- Seminar, CS Department, Mc Gill University, Montreal, Canada, 20 septembre 2000.

[67]
P. Cousot. -- On the design of abstractions for software checking. -- 12 février 2001. Microsoft Research, Redmond, WA, USA.

[68]
P. Cousot. -- From semantics to types systems by abstract interpretation. -- 15 janvier 1998. Séminaire AFPLC « Typages ».

[69]
P. Cousot. -- The Marktoberdorf '98 generic abstract interpreter. -- novembre 1998. http://www.di.ens.fr/~cousot/Marktoberdorf98.shtml.

[70]
P. Cousot. -- Refining model checking by abstract interpretation. -- 24 septembre 1998. Dip. di Informatica, Univ. di Udine, Italie.

[71]
P. Cousot. -- Interprétation abstraite et analyse statique. -- 26 mai 1999. 10eme anniversaire du LIX, École polytechnique, Palaiseau.

[72]
P. Cousot. -- Design of semantics by abstract interpretation. -- 2 juin 1997. MPI-Kolloquium, Max-Planck-Institut für Informatik Im Stadtwald, Sarrebruck, DE.

[73]
P. Cousot. -- Interprétation abstraite temporelle. -- 11 janvier 2000. Séminaire de l'IRISA, Rennes.

[74]
P. Cousot. -- Partial completeness of abstract fixpoint checking. -- 13 juin 2000. ROPAS seminar, EECS Dept., KAIST, Taeduk Science Complex, Taejon, République de Corée.

[75]
P. Cousot et R. Cousot. -- Abstract interpretation, temporal logic and data flow analysis. -- 11--16 avril 1999. Dagstuhl Seminar 99151 on Program Analysis, Schloß Dagstuhl, Wadern, Allemagne.

[76]
J. Feret. -- Pi s.a. : Analyse statique de code mobile par interprétation abstraite. Prototypes, http://www.di.ens.fr/~feret/prototypes/.

[77]
L. Mauborgne. -- Graphes de décision binaire. -- juin 1999. Séminaire SIA de l'ENS, Paris.

[78]
L. Mauborgne. -- Representation of sets of trees for abstract interpretation. -- 8 mars 2000. Séminaire « Internet Technologies Meetings » de l'ITUC, Copenhague.

[79]
L. Mauborgne. -- Representation of sets of trees for abstract interpretation. -- 30 novembre 2000. Séminaire de l'ULB, Bruxelles.

[80]
L. Mauborgne. -- Représentation d'ensembles d'arbres. -- 31 janvier 2000. Séminaire du LIAFA, Paris.

[81]
L. Mauborgne. -- Représentation d'ensembles d'arbres pour l'interprétation abstraite. -- 13 mars 2000. ENS, Paris.

[82]
L. Mauborgne. -- Sets of trees and abstract interpretation. -- 11 avril 2000. Séminaire du MPI, Sarrebruck.

[83]
D. Monniaux. -- The Absinthe abstract interpreter. Prototypes, http://cgi.dmi.ens.fr/cgi-bin/monniaux/absinthe.

[84]
D. Monniaux. -- Efficient storage for storing the country of internet protocol domains. -- 2001.