[Version française]

Weakly Relational Numerical Abstract Domains

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

Ph.D Laboratoire d'Informatique de l' école Normale Supérieure (Paris)

Ph.D Report

Acrobat PDF (2.5 MB)

Compressed PostScript .PS.GZ (1.2 MB)

Defense slides

Acrobat PDF


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-Yc), the zone congruence domain (XY+c [b]), and the octagon domain (±X ±Yc), 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.

Pictures of the defense!

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é