My PHD thesis :
Abstract Acceleration to improve precision in Linear Relation Analysis
October, 25th,2007, 2pm (14H), MJK, Grenoble

Jury

Abstract (FR + EN)


This work deals with verification of safety properties of programs, and more specifically with numerical properties. Linear Relation Analysis, which is an abstract interpretation based on a approximation of numerical states by convex polyhedra, has proved its efficiency. It consists in generating polyhedral overapproximations of the set of valuations associated to each control point. The introduction of a widening operator ensures the convergence of the analyses. However in some cases the invariants generated are not precise enough and improving the precision by delaying the widening is too costly. That is why we have considered so-called acceleration methods, which consist in computing the exact effect of one or several loops (as Presburger formulae). The main drawback of these methods is that they apply only to a restricted class of programs.

In this thesis, we propose an approach combining the classical Linear Relation Analysis (with widening) and the notion of Abstract Acceleration which is useful in order to compute a precise overapproximation of the iterate application of certain types of loops. We aim at improving the precision of the analyses while always guaranteeing termination. The first experimental results obtained thanks to our tool Aspic have allowed to validate the method, which increase both precision and efficacity.

Keywords: Numerical Properties Verification, Generation of polynomial Invariants, Linear Relation Analysis, Widening, Abstract Acceleration, Aspic.

Le travail décrit dans cette thèse s'inscrit dans le contexte de la validation de propriétés de sûreté de programmes, et plus particulièrement des propriétés numériques. L'utilisation de la technique d'Analyse des Relations Linéaires, une interprétation abstraite fondée sur une approximation des états numériques par des polyèdres convexes, a fait ses preuves dans le domaine. Il s'agit de générer des surapproximations polyédriques de l'ensemble des valuations associées à chaque point de contrôle, l'introduction d'un opérateur d'élargissement assurant la convergence des analyses. Cependant dans certains cas les invariants générés ne sont pas assez précis, et l'amélioration de la précision via le retardement du moment d'application de l'élargissement est trop via le retardement du moment d'application de l'élargissement est trop coûteux. Nous nous sommes donc intéressés aux méthodes dites d'accélération, qui consistent à calculer exactement l'effet d'une ou plusieurs boucles (sous la forme de formules de Presburger), le principal inconvénient de ces méthodes étant qu'elles ne s'appliquent qu'à une classe restreinte de programmes.
Dans cette thèse nous proposons une approche combinant l'Analyse des Relations Linéaires classique (avec élargissement) et la notion d'Accélération abstraite utile pour calculer une surapproximation précise de l'application itérée de certains types de boucles, dans le but d'améliorer la précision des analyses tout en garantissant toujours la terminaison. Les premiers résultats expérimentaux obtenus grâce à l'implémentation de l'analyseur Aspic ont permis de valider la méthode, qui a le principal avantage de combiner amélioration de la précision et efficacité.

Mots-clés : Vérification de propriétés numériques, Génération d'invariants polynomiaux, Analyse des Relations Linéaires, Élargissement, Accélération Abstraite, Aspic.

Manuscrit (FR)