Defended on Monday 6 December 2004
The jury was:
|Patrick COUSOT||Professor, École Normale Supérieure (Paris)||Ph.D Advisor|
|Chris HANKIN||Professor, Imperial College, London||President|
|Roberto GIACOBAZZI||Professor, Università degli Studi di Verona||Reviewer|
|Helmut SEIDL||Professor, Technische Universität München||Reviewer|
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.
Merci à / Courtsey Guillaume Capron, Yves Verhoeven.