Ph.D

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

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.

Pictures of the defense!

Merci à / Courtsey Guillaume Capron, Yves Verhoeven.

Antoine Miné