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
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.