Accélération abstraite pour l'amélioration de la précision en Analyse des Relations Linéaires
gonnord Laure Danthony · HAL (Le Centre pour la Communication Scientifique Directe) · 2007
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.