Skip to Main content Skip to Navigation

Weakly Relational Numerical Abstract Domains

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.
Complete list of metadata

Cited literature [114 references]  Display  Hide  Download
Contributor : Antoine Miné Connect in order to contact the contributor
Submitted on : Wednesday, March 14, 2007 - 5:20:59 PM
Last modification on : Thursday, March 17, 2022 - 10:08:25 AM
Long-term archiving on: : Friday, September 21, 2012 - 12:55:37 PM


  • HAL Id : tel-00136630, version 1



Antoine Miné. Weakly Relational Numerical Abstract Domains. Software Engineering [cs.SE]. Ecole Polytechnique X, 2004. English. ⟨tel-00136630⟩



Record views


Files downloads