Note publique d'information : 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é.
Note publique d'information : 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.
paprika.idref.fr
data.idref.fr
Documentation
