Soutenance de Thèse, Antoine Miné

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

Mémoire de thèse / PhD. Report

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-Y≤c, des zones de congruence (X≡Y+c [b]) et des octogones (±X ±Y≤c). 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.

Abstract

The goal of this thesis is to design techniques related to the automatic analysis of computer programs. One major application is the creation of tools to discover bugs before they actually happen, an important goal in a time when critical yet complex tasks are performed by computers. We will work in the Abstract Interpretation framework, a theory of sound approximation of program semantics. We will focus, in particular, on numerical abstract domains that specialize in the automatic discovery of properties of the numerical variables of programs.
In this thesis, we introduce new numerical abstract domains: the zone abstract domain (that can discover invariants of the form X-Y≤c), the zone congruence domain (X≡Y+c [b]), and the octagon domain (±X ±Y≤c), among others. These domains rely on the classical notions of potential graphs, difference bound matrices, and algorithms for the shortest path closure computation. They are in-between, in terms of cost and precision, between non-relational domains (such as the interval domain), that are very imprecise, and classical relational domains (such as the polyhedron domain), that are very costly. We will call them “weakly relational.” We also introduce some methods to apply relational domains to the analysis of floating-point numbers, which was previously only possible using imprecise, non-relational domains. Finally, we introduce so-called “linearization” and “symbolic constant propagation” generic methods to enhance the precision of any numerical domain, for a low increase in cost.
The analysis framework presented in this thesis has been integrated within Astrée, an analyzer for critical embedded software, and were instrumental in proving the absence of run-time errors in fly-by-wire softwares. Experimental results show the usability of our methods in the context of real-life applications.