Fraction : analyseur de propriétés par des techniques de résolution de contraintes

F. Parrennes

LIP6 2001/017: Rapport de Recherche LIP6 / LIP6 research reports
14 pages - Juin/June 2001 - French document.

Get it : 310 Ko /Kb

Contact : par mail / e-mail

Thème/Team: Sémantique, Preuve et Implantation

Titre français : Fraction : analyseur de propriétés par des techniques de résolution de contraintes
Titre anglais : Fraction : properties analysis by constraint computation

Résumé : Ce papier décrit Fraction, un outil de vérification de propriétés de programme par utilisation de contraintes. L'utilisation de techniques liées aux contraintes pour vérifier des propriétés n'est pas véritablement nouvelle.
L'originalité de l'approche exposée est d'avoir défini une traduction d'un langage de style impératif en une série de systèmes de contraintes. Ce sont les algorithmes de résolution de contraintes qui permettent de valider ou non les propriétés recherchées. Cette traduction passe par une étape intermédiaire où l'on retrouve l'aspect fonctionnel des programmes.
L'utilisation du langage Ocaml a permis de réaliser facilement un prototype de la méthode dont l'architecture rappelle celle d'un compilateur. La définition d'un solveur de contraintes modulaire rend l'outil paramétrable par rapport à des modules de résolution de contraintes sur des domaines différents (les entiers et les booléens par exemple).

Abstract : This paper describes the tool Fraction which use constraint computation for properties verification.
Constraints have already been used for properties validation, however our approach try to translate complete imperative programs into constraint systems.
Thus, we are using some classical algorithms of constraints computation to validate initial properties. Firstly, this translation tried to find the functionnal behavior of programs, secondely the functionnal behavior is translate into constraint systems.
A prototype of the tool have been carry out using Ocaml language and based on a compiler scheme. The definition of a modular constraints satisfaction tool allows Fraction to be parametrized by several constraints domains.

Mots-clés : Analyse statique, vérification de propriétés, résolution de contraintes

Key-words : Static analysis, properties verification, constraint computation

Publications internes LIP6 2001 / LIP6 research reports 2001

Responsable Éditorial / Editor :David.Massot@lip6.fr