Weakly Relational Numerical Abstract Domains

`THESE
pr´esent´ee a`
´l’ECOLE POLYTECHNIQUE
pour l’obtention du titre de
´DOCTEUR DE L’ECOLE POLYTECHNIQUE
EN INFORMATIQUE
´Antoine MINE
6 d´ecembre 2004
Domaines num´eriques abstraits
faiblement relationnels
Weakly Relational Numerical Abstract Domains
Pr´esident: Chris Hankin
Professeur, Imperial College, Londres
Rapporteurs: Roberto Giacobazzi
Professeur, Universita` degli Studi di Verona
Helmut Seidl
Professeur, Technische Universitat Munchen¨ ¨
Examinateur: Nicolas Halbwachs
Directeur de recherche CNRS, VERIMAG, Grenoble
Directeur de th`ese: Patrick Cousot
´Professeur, Ecole Normale Sup´erieure, Paris
´Ecole Normale Sup´erieure
D´epartement d’InformatiquecAntoine Min´e, 2004.
´Cette recherche a ´et´e conduite `a l’Ecole Normale Sup´erieure de Paris durant un contrat
d’allocationcoupl´ee(normalien)del’Universit´eParisIXDauphine. Cetterecherchea´et´efi-
nanc´eeenpartieparlesprojetsDaedalus(projeteurop´eenIST-1999-20527duprogramme
´FP5) et Astree (projet franc¸ais RNTL).
Lesopinionspr´esent´eesdanscedocumentsontcellespropresdesonauteuretnerefl`etenten
´ ´aucun cas celles de l’Ecole Polytechnique, de l’Universit´e Parix IX Dauphine, ou de l’Ecole
Normale Sup´erieure de Paris.´ ´RESUME iii
R´esum´e
Le sujet de cette th`ese est le d´eveloppement de m´ethodes pour l’ana-
lyse automatique des programmes informatiques. Une des applications
majeures est la conception d’outils pour d´ecouvrir les erreurs de pro-
grammation avant qu’elles ne se produisent, ce qui est crucial ...