[English version]

Domaines numériques abstraits faiblement relationnels


soutenue le Lundi 6 décembre 2004

devant le jury composé de:

Patrick COUSOT    Professeur, École Normale Supérieure (Paris)   Directeur de thèse
Chris HANKIN    Professeur, Imperial College, Londres   Président du jury
Roberto GIACOBAZZI   Professeur, Università degli Studi di Verona   Rapporteur
Helmut SEIDL    Professeur, Technische Universität München   Rapporteur


Thèse éffectuée au Laboratoire d'Informatique de l' école Normale Supérieure (Paris)

Mémoire de thèse

Acrobat PDF (2.5 MB)

PostScript .PS.GZ (1.2 MB)

Transparents de la soutenance

Acrobat PDF

Résumé

Le sujet de cette thèse est le développement de méthodes pour l'analyse automatique des programmes informatiques. Une des applications majeures est la conception d'outils pour découvrir les erreurs de programmations avant qu'elles ne se produisent, ce qui est crucial l'heure où des tâches critiques mais complexes sont confiées des ordinateurs. Nous nous plaçons dans le cadre de l'interprétation abstraite, qui est une théorie de l'approximation sûre des sémantiques de programmes, et nous nous intéressons en particulier aux domaines abstraits numériques spécialisés dans la découverte automatique des propriétés des variables numérique d'un programme.

Dans cette thèse, nous introduisons plusieurs nouveaux domaines numériques abstraits et en particulier le domaine des zones (permettant de découvrir des invariants de la forme X-Yc, des zones de congruence (XY+c [b]) et des octogones (±X ±Yc). Ces domaines sont basés sur les concepts existants de graphe de potentiel, de matrice de différences bornées et sur l'algorithmique des plus courts chemins. Ils sont intermédiaires, en terme de précision et de coût, entre les domaines non relationnels (tel celui des intervalles), très peu précis, et les domaines relationnels classiques (tel celui des polyèdres), très coûteux. Nous les nommons « faiblement relationnels ». Nous présentons également des méthodes permettant d'appliquer les domaines relationnels l'analyse de nombres virgule flottante, jusqu' présent uniquement réalisable par des domaines non relationnels donc peu précis. Enfin, nous présentons des méthodes génériques dites de « linéarisation » et de « propagation de constantes symboliques » permettant d'améliorer la précision de tout domaine numérique, pour un surcoût réduit.

Les méthodes introduites dans cette thèse ont été intégrées Astrée, un analyseur spécialisé dans la vérification de logiciels embarqués critiques et se sont révélées indispensables pour prouver l'absence d'erreurs l'exécution de logiciels de commande de vol électrique. Ces résultats expérimentaux viennent justifier l'intérêt de nos méthodes pour des cadre d'applications réelles.

Photos de la soutenance!

Merci à / Courtsey Guillaume Capron, Yves Verhoeven.

[A picture] [A picture] [A picture]
[A picture] [A picture] [A picture]
[A picture] [A picture] [A picture]
[A picture]



Antoine Miné