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.

This document was translated from LATEX by HEVEA.