LIP6 2001/017
- Reports
Fraction : analyseur de propriétés par des techniques de résolution de contraintes - F. Parrennes
- 14 pages - 06/25/2001- document en - http://www.lip6.fr/lip6/reports/2001/lip6.2001.017.pdf - 317 Ko
- Contact : Fabrice.Parrennes (at) nulllip6.fr
- Ancien Thème : SPI
- Keywords : Static analysis, properties verification, constraint computation
- Publisher : David.Massot (at) nulllip6.fr
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.
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.