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
-
Responsable :
- Patrick Cousot,
professeur ý l'ENS ;
- Autre membre permanent :
- Laurent Mauborgne,
maÓtre de confÈrences ý l'ENS depuis sept. 2000 ;
- Doctorants :
- JÈrÙme Feret,
ÈlËve normalien en 4eme annÈe,
et doctorant depuis juin 2000 ;
- Antoine MinÈ,
ÈlËve normalien en 4eme annÈe,
stagiaire puis doctorant depuis juin 2000 ;
- David Monniaux,
ÈlËve normalien de septembre 1998 ý aošt 1999, assistant moniteur
normalien ý l'UniversitÈ de Paris IX (Dauphine) depuis septembre
1999 ;
- Frank VÈdrine,
assistant moniteur
normalien, 9/1997 -- 9/2000.
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'analyse des interfÈrences permet de dÈtecter quels
processus sont susceptibles d'interagir parce qu'ils communiquent sur
un mÍme canal ou qu'ils sont localisÈs sur un mÍme site.
Nous avons rÈalisÈs une analyse des interfÈrences ý la
fois dans le cas de la mobilitÈ implicite [28] et
dans celui de la mobilitÈ explicite [59]. Ces
analyses permettent de distinguer les objets crÈÈs par des
instances rÈcursives de processus, ce qui est fondamental dans
l'Ètude de la mobilitÈ ;
- une analyse du nombre de processus ou analyse de forme, qui
permet de dÈtecter, indÈpendamment des objets qui leur sont
communiquÈs, quelle est la rÈpartition des processus dans le
systËme. Nous avons rÈalisÈ une analyse qui permet de
compter le nombre de processus utilisÈs par un systËme mobile,
dans le cas de la mobilitÈ implicite [14].
Elle fait apparaÓtre des exclusions mutuelles et permet de garantir
le non-Èpuisement des ressources.
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 :
-
la rÈutilisation des techniques d'interprÈtation abstraite dÈjý
existantes, y compris si possible au niveau de l'implantation ;
- l'exactitude mathÈmatique de l'analyse ; en particulier,
l'analyse ne devra pas introduire des hypothËses supplÈmentaires sur
les probabilitÈs (par exemple l'indÈpendance de certaines
variables).
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:
-
sÈmantique dÈnotationnelle en avant (suivant Kozen et
[35]) ;
- sÈmantique dÈnotationnelle en arriËre (adjoint linÈaire de la
prÈcÈdente) [37].
Nous avons dÈveloppÈ des treillis abstraits adaptÈs ý ces sÈmantiques :
-
sommes finies [35] ;
- localisation des mesures [35] ;
- gaussiennes ;
- queues sous-exponentielles (permettant l'analyse de terminaison
de certains programmes et la validation d'analyses statistiques de
temps moyens) [62].
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
-
Contrats europÈens :
-
DAEDALUS: Validation of critical software by static analysis
and abstract testing.
P. Cousot (ENS, coordinateur scientifique), R. Cousot (Šcole
polytechnique), A. Deutsch (Polyspace technologies), C. Ferdinand
(AbsInt), Š. Goubault (CEA), N. Jones (DIKU), A. Deutsch & D. Pilaud
(Polyspace technologies), F. Randimbivololona (EADS-Airbus,
coordinateur administratif), M. Sagiv (U. Tel Aviv), H. Seidel (U.
TrËves) et R. Wilhelm (U. Sarrebruck).
Project IST-1999-20527 of the european 5th Framework
Programme (FP5), oct. 2000 -- oct. 2002.
-
Abstract interpretation of mobile processes.
P. Cousot (ENS) et C. Priami (U. Pise).
Specific research and technological development programme in the field of the training and mobility of researchers
(TMR) FMBI961050, oct. 1996 -- sep. 1997.
-
ABILE: Abstract interpretation for declarative
languages.
R. Barbuti (U. de Pise),
M. Bruynooghe (U. de Louvain),
P. Codognet (INRIA Rocquencourt),
M.-M. Corsini (U. de Bordeaux),
P. Cousot (ENS),
R. Cousot (Šcole polytechnique),
P. Devienne (U. de Lille),
G. FilË (U. de Padoue),
M. Hanus (Max-Planck-Institut f¸r Informatik, Saarbr¸cken),
M. Hermenegildo (U. polytechnique de Madrid),
N. Jones (U. de Copenhagen),
B. L. Charlier (FacultÈs U. de Namur),
G. Levi (U. de Pise),
J. Mauszynski (U. de Link–ping),
A. Mycroft (U. de Cambridge)
et U. Nilsson (U. de Link–ping).
Human capital and mobility (HCM) european network, jan. 1995 -- dÈc. 1997.
- Contrats bilatÈraux (programmes d'actions intÈgrÈes) :
-
Model-checking et analyse statique.
P. Cousot (ENS) et A. Podelski (Max-Planck-Institut f¸r
Informatik).
Programme d'actions intÈgrÈes franco-allemandes
Procope, jan. 2000 -- dÈc. 2000.
-
SÈcuritÈ de systËmes distribuÈs
par interprÈtation abstraite.
P. Cousot (ENS) et R. Giacobazzi (U. VÈrone).
Programme d'actions intÈgrÈes franco-italiennes
GalilÈe, jan. 1999 -- dÈc. 2000.
- Contrats franÁais :
- Contrats institutionnels franÁais :
-
Validation de code mobile par interprÈtation abstraite.
P. Cousot (ENS).
Projet TL97130 du programme TÈlÈcommunications du CNRS, jan. 1997 --
dÈc. 1999.
-
TUAMOTU: Tatouage Èlectronique sÈmantique de code
mobile JavaTM.
P. Cousot (ENS), R. Cousot (Šcole polytechnique) et M. Riguidel (Thales Communications).
Project RNRT 1999 nƒ 95, oct. 1999 --
oct. 2001.
-
Analyses statiques probabilistes.
P. Cousot (ENS) et Š. Goubault (CEA).
Contrat ENS --- CEA, nƒ SAV 27234/VSF, jan. 1999 --
dÈc. 2001.
- Contrats industriels :
-
Štude des procÈdÈs de signature logicielle pour
les objets mobiles Ècrits en JavaTM.
P. Cousot (ENS) et M. Riguidel (Thales Communications).
Contrat ENS --- Thales Communications, jan. 1999 -- dÈc.
2000.
-
La vÈrification statique de propriÈtÈs temporelles de
logiciels avioniques par interprÈtation abstraite.
P. Cousot (ENS) & F. Randimbivololona (EADS Airbus).
Contrat ENS -- EADS Airbus, juin 2001 -- juin 2003.
- Groupes de travail internationaux :
P. Cousot est membre du groupe de travail WG 2.3 de l'IFIP sur la
<< mÈthodologie de la programmation >>. Il participe ý ses rÈunions de
travail [39] ou les organise rÈguliËrement en France
[38].
2 Missions, confÈrences et sÈminaires
- P. Cousot :
- sÈminaires
au Max-Planck-Institut f¸r Informatik (Sarrebruck, Allemagne -- juin 1997) [72],
ý Obernai (septembre 1997) [38],
KAIST (Taejon, RÈpublique de CorÈe -- novembre 1997) [48],
Paris (janvier 1998) [68],
Udine (Italie -- septembre 1998) [70],
Dagstuhl Seminar 99151 (Allemagne -- avril 1999) [75],
Paris (mai 1999) [71],
Rennes (janvier 2000) [73],
KAIST (Taejon, RÈpublique de CorÈe -- juin 2000) [22, 74],
MontrÈal (Canada -- septembre 2000) [66] ;
- confÈrences
Paris (septembre 1997) [9],
Sydney (Australie -- dÈcembre 1997) [26],
Valence (Espagne -- juin 1998) [20],
Pise (Italie, SAS'98 -- septembre 1998),
Padoue (Italie -- mai 1999) [18],
Venise (Italie, SAS'99 -- septembre 1999),
Paris (ICFP'99 & PPDP'99, septembre 1999),
Osaka (Japon -- novembre 1999) [21],
Boston (USA, PEPM'00 -- janvier 2000),
Boston (USA -- janvier 2000) [27],
Schloþ Ringberg (Allemagne -- fÈvrier 2000) [25],
Santa Barbara (USA, LICS'00 & SAS'00 -- juin 2000),
Austin (USA -- juillet 2000) [8, 65],
L'Aquila (Italie -- aošt 2000) [6, 10],
Sarrebruck (Allemagne -- aošt 2000) [23],
MontrÈal (Canada, ICFP'99 & PPDP'99, septembre 1999),
La RÈunion (novembre 2000) [17],
Santa Cruz (USA -- janvier 2001) [39],
Londres (UK, CW'01 & POPL'01 -- janvier 2001),
Redmond (USA -- fÈvrier 2001) [67],
Munich (Allemagne -- mars 2001) [24],
GÍnes (Italie, ESOP'01, ETAPS'01 & TACAS'01 -- avril 2001) ;
- cours ý
Taejon (RÈpublique de CorÈe -- novembre 1997) [48],
Nantes (avril 1998) [51],
Udine (Italie -- septembre 1998) [50],
Paris (IENS--X, janvier 1999) [52],
Marktoberdorf (Allemagne -- juillet/aošt 1998) [49, 56, 69],
Paris (ASPROM, octobre 2000) [53].
- JÈrÙme Feret :
- sÈminaires ý
l'Šcole normale supÈrieure (mars et novembre 2000),
P.P.S. (Chevaleret, janvier 2001),
LORIA, Nancy (janvier 2001) ;
- confÈrences ý
Pise (SAS'98, septembre 1998),
Venise (SAS'99, septembre 1999),
Paris (ICFP'99, septembre 1999),
Paris (PPDP'99, septembre 1999),
Santa Barbara (SAS'00, juin 2000) [28],
State College (GETCO'00, USA, aošt 2000) [14],
State College (CONCUR'00, USA, aošt 2000).
- Laurent Mauborgne :
- sÈminaires ý
Paris (juin 1999) [77],
Paris (janvier 2000) [80],
Copenhague (Danemark -- mars 2000) [78],
Paris (mars 2000) [81],
Saarbr¸ck (Allemagne -- avril 2000) [82],
Bruxelles (Belgique -- dÈcembre 2000) [79] ;
- confÈrences ý
Pise (SAS'98, Italie -- septembre 1998),
Venise (Italie -- septembre 1999) [29],
Berlin (Allemagne -- mars 2000) [30],
Santa Barbara (USA -- juin 2000) [31],
Londres (POPL'01, UK -- janvier 2001),
GÍnes (ETAPS'01, Italie -- avril 2001) ;
- cours ý Copenhague (Danemark -- fÈvrier-mars 2000)
[57] ;
- sÈjour ý Saarbr¸ck (Allemagne -- avril-mai 2000).
- Antoine MinÈ :
- sÈminaire ý
Grenoble (novembre 2000) ;
- confÈrence ý
Santa Barbara (USA -- juin 2000) ;
- Ècole d'ÈtÈ ý Cahmina (Portugal -- septembre 2000).
- David Monniaux :
- sÈminaires ý
Dagstuhl (Allemagne -- avril-mai 2000),
Londres (Royaume--Uni -- avril 2000),
G–teborg (SuËde -- juin 2000) ;
- confÈrences ý
Mordano (CSFW'12, Italie -- juin 1999) [34],
Venise (SAS'99, Italie -- septembre 1999) [33],
Santa Barbara (SAS'00, USA -- juillet 2000) [35],
Sarrebruck (Allemagne -- aošt 2000),
Londres (POPL'01, UK -- janvier 2001) [36],
GÍnes (ESOP'01, Italie -- avril 2001) [37].
3 Accueil de chercheurs
- Professeurs et directeurs de recherche invitÈs
- Peter Lee (Carnegie Mellon University), juillet 1997.
(Professeur invitÈ ENS) ;
- David Schmidt (Kansas State University), juin 1998.
(Professeur invitÈ ENS) ;
- Reinhard Wilhelm (Universit”t des Saarlandes),
septembre 1999. (Professeur invitÈ ENS) ;
- Andreas Podelski (Max-Planck-Institut f¸r
Informatik), mars 2000. (Professeur invitÈ ENS) ;
- Barbara Ryder (Rutgers University), mai 2001.
(Professeur invitÈ ENS).
- Neil Jones (DIKU, UniversitÈ de Copenhague), octobre 2001.
(Professeur invitÈ).
- Post-doctorants
- Sven-Olof Nystr–m (Uppsala Universitet, oct. 1996 --
sep. 1997).
- Corrado Priami (Universitý di Pisa,
oct. 1996 -- sep. 1997).
- Germ·n Puebla S·nchez (Universidad PolitÈcnica
de Madrid), octobre 1997 -- dÈcembre 1997.
- Jean-FranÁois Raskin (F.U.N.D.P., Namur), octobre 1997
-- dÈcembre 1997.
- Arnaud Venet (Contrat ENS --- Thales Communications),
mars 1999 -- juillet 1999.
4 Diffusion de la connaissance
- Accueil ý l'ENS du ´ Symposium international sur l'analyse
statique ª, 8--10 septembre 1997.
- P. Cousot anime et organise ý l'ENS le sÈminaire SIA
´ SÈmantique et interprÈtation abstraite ª. Ce
sÈminaire accueille occasionnellement des orateurs prestigieux mais a
principalement pour objet de permettre ý de jeunes chercheurs franÁais
ou Ètrangers de prÈsenter leurs travaux et de les voir discutÈs.
Une vingtaine d'exposÈs ont lieu chaque annÈe.
http://www.di.ens.fr/~cousot/annonceseminaire.shtml
- Cours de formation de P. Cousot pour ingÈnieurs de l'industrie
(Institut de l'ENS -- CollËge de Polytechnique [52],
ASPROM [53]) ;
- P. Cousot est coordinateur scientifique du projet europÈen
DAEDALUS
(FP5//IST-/-1999-/-20527,
oct. 2000 -- oct. 2002).
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.
- P. Cousot a dÈveloppÈ un prototype d'analyseur
statique gÈnÈrique ainsi que divers domaines abstraits ý but
pÈdagogique [69] qui est disponible sur la toile
http://www.di.ens.fr/~cousot/Marktoberdorf98.shtml ;
- P. Cousot et A. Venet ont dÈveloppÈ un
tatoueur de mÈthodes de classes
JavaTM dans le cadre du contrat
TUAMOTU [58] ;
- J. Feret a implantÈ un analyseur pour les systËmes
mobiles spÈcifÌÈs en p-calcul [76]. Le propotype
est disponible sur la toile
http://www.di.ens.fr/~feret/prototypes/ ;
- A. MinÈ a programmÈ un prototype d'analyseur
statique basÈ sur les domaines numÈriques abstraits
[32, 61] ;
- D. Monniaux a dÈveloppÈ un analyseur de protocoles
cryptographiques par interprÈtation abstraite dans un domaine
d'automates d'arbres ;
- D. Monniaux a dÈveloppÈ un analyseur de programmes
probabilistes Ècrits dans un sous-ensemble du langage C. Cet analyseur
est disponible sur la Toile en tÈlÈchargement
(http://www.di.ens.fr/~monniaux/download/absinthe.tar.gz) et en
consultation directe
(http://cgi.dmi.ens.fr/cgi-bin/monniaux/absinthe) ;
- D. Monniaux a dÈveloppÈ des bibliothËques d'interfaÁage
entre le langage Objective Caml et les librairie GMP (calcul
scientifique) et Gtk ; ces bibliothËques sont mises ý disposition sur
la toile (http://www.di.ens.fr/~monniaux/programmes.html.fr) ;
- D. Monniaux a dÈveloppÈ un classificateur d'adresses IP
selon leur origine gÈographique utilisant des structures de donnÈes
habituellement utilisÈes pour l'analyse de programmes.
6 Participation ý l'Èvaluation de la recherche
- P. Cousot :
- Membre du comitÈ de rÈdaction de la revue SCP (jusqu'en 2000) ;
- PrÈsident du comitÈ de programme de SAS'01 ;
- Membre du comitÈ de programme de GETCO'00, GETCO'01, SAS'99,
SAS'00, WSAGV'2000 ;
- Švaluateur pour les confÈrences internationales
ECOOP'00,
ESOP'99
ESOP'00,
ESOP'01,
KR'00,
LICS'99
PEPM'97,
PLDI'01,
PLI'99,
POPL'97,
SAIG'00,
SAS'97 et
SAS'98 ;
- Švaluateur pour les journaux ACM Computing Surveys, ACM TOPLAS,
Acta Informatica, SCP, JACM, JASE, TCS ;
- Švaluateur pour les soumissions de projets
europÈens IST (FP 5 RTD Programmes),
autrichiens << Fonds zur F–rderung der wissenschaftlichen Forschung >> (FWF),
italiens (Istituto Superiore Mario Boella, ISMB et << Centre International des Sciences MÈcaniques >> (CISM), Udine),
finlandais (Finish Programme for Centers of Excellence in Research 2001--2007 de l'acadÈmie de Finlande),
nÈerlandais << Stichting informatica-onderzoek in Nederland >> (SION, the Netherlands Computer Science Research Foundation) pour le compte de << the Netherlands Organisation for Scientific Research (NWO) >> ;
- Švaluateur pour le projet europÈen Esprit LTR project 23498 vires, Prof. P. Wolper (coordinateur) ;
- Membre du conseil scientifique du dÈpartement EECS du KAIST
(Taeduk Science Complex, Taejon, RÈpublique de CorÈe) ;
- Expert pour le recrutement d'enseignants et chercheurs
(Ben-Gurion University of the Negev (IsraÎl),
Carnegie Melon University (Computer Science Department),
Imperial College of Science, Technology and Medicine de Londres (UK),
Rutgers University, New Jersey, (Computer Science Department),
UniversitÈ de Cambridge (UK),
UniversitÈ de Melbourne (Australie),
UniversitÈ de Sarrebr¸ck (Allemagne)).
- J. Feret :
- Švaluateur pour les confÈrences ESOP'00, PPDP'00, ESOP'01 et
SAS'01.
- L. Mauborgne :
- Švaluateur pour les confÈrences POPL'97, FMPPTA'97,
FMPPTA'98, ICCL'98, SAS'99, ESOP'00, PPDP'00, ESOP'01 et
SAS'01.
- A. MinÈ :
- Švaluateur pour les confÈrences ESOP'01, PADO'01 et SAS'01.
- D. Monniaux :
- Švaluateur pour les confÈrences FMPPTA'99, FMPPTA'00,
FMPPTA'01, ESOP'01 et SAS'01.
7 Encadrement doctoral
-
Direction de thËses
- P. Cousot :
- J. Goubault, Logique, complexitÈ,
dÈmonstration automatique et thËmes annexes
[42], Habilitation ý diriger les
recherches, UniversitÈ de Paris 9, Dauphine, soutenue le 27 juin
1997 ;
- L. Mauborgne, ReprÈsentation d'ensembles
d'arbres pour l'interprÈtation abstraite
[43], ThËse de doctorat de
l'Šcole polytechnique en informatique, soutenue
le 25 novembre 1999 ;
- F. VÈdrine, Analyses totales de
programmes par l'interprÈtation abstraite
[44], ThËse de doctorat de
l'Šcole polytechnique en informatique, soutenue
le 28 janvier 2000.
- P. Cousot et D. Parigot :
- L. Correnson, SÈmantique
Èquationelle [41], ThËse de
doctorat de l'Šcole polytechnique en
informatique, soutenue le 1er avril 2000.
- P. Cousot et A. Deutsch :
- B. Blanchet, Analyse d'Èchappement,
Applications ý ML et JavaTM
[40], ThËse de doctorat de l'Šcole
polytechnique en informatique, soutenue le 7
dÈcembre 2000.
- P. Cousot, direction de thËses en cours :
J. Feret, A. MinÈ et D. Monniaux.
- Participation ý d'autres jurys de thËses
-
P. Cousot : 7 jurys dont 1 prÈsidence et 3 rapports.
- Direction de projets de DEA
-
P. Cousot :
- D. MassÈ, InterprÈtation abstraite du langage de
programmation LUSTRE [45]. 1998 ;
- D. Monniaux, RÈalisation mÈcanisÈe d'interprÈteurs abstraits
[47]. 1998 ;
- A. MinÈ, ReprÈsentation d'ensembles de contraintes
de somme ou de diffÈrence de deux variables et application ý
l'analyse automatique de programmes [46]. 2000.
8 Enseignement
-
DeuxiËme cycle
-
P. Cousot :
- Directeur des Ètudes pour l'informatique ý l'ENS ;
- Responsable du magistËre MMFAI pour l'informatique ;
- Cours << Langages de programmation et compilation >> au MMFAI [54];
- Cours << SÈmantiques des langages de programmation >> au MMFAI [55].
- L. Mauborgne :
- TDs d'algorithmique ý l'Šcole polytechnique (1997-99 et 2000-01) ;
- TDs de compilation au MMFAI (1999-2001) ;
- TDs d'algorithmique et programmation au MMFAI (1999-2001).
- A. MinÈ :
- Encadrement de travaux dirigÈs pour le cours de programmation
systËme ý l'Šcole polytechnique (2001).
- D. Monniaux :
- Travaux dirigÈs et pratiques d'algorithmique et programmation
en premiËre annÈe de DEUG MASS ý l'UniversitÈ Paris 9 Dauphine ;
- Participation ý l'Èvaluation des stages en entreprise ý l'Šcole
Nationale SupÈrieure de Techniques AvancÈes (1999).
- TroisiËme cycle
- P. Cousot :
- Cours Fondement de l'interprÈtation abstraite du
DEA << Programmation : sÈmantique, preuves et langages >>.
- Cours de P. Cousot ý des Šcoles pour jeunes chercheurs
[51] ;
- Cours de doctorat de P. Cousot sur l'interprÈtation abstraite ý
l'Ètranger (KAIST, RÈpublique de CorÈe [48],
UniversitÈ d'Udine [50], << NATO Int. Summer School
1998 on Calculational System Design >> de Marktoberdorff
[56]) ;
- J. Feret :
- Participation au cours << Analyse statique par interprÈtation
abstraite >> de Radhia Cousot, dans le cadre du DEA << Programmation :
sÈmantique, preuves et langages >> (2001).
- L. Mauborgne :
- Participation au cours<< Analyse statique par interprÈtation
abstraite >> de Radhia Cousot, dans le cadre du DEA << Programmation :
sÈmantique, preuves et langages >> (1999-2001) ;
- Cours sur les reprÈsentations d'ensembles d'arbres en analyse de
programme ý l'UniversitÈ de Copenhague (2000) [57].
- D. Monniaux :
- Participation au cours << Analyse statique par interprÈtation
abstraite >> de Radhia Cousot, dans le cadre du DEA << Programmation :
sÈmantique, preuves et langages >> (2001).
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.