Home |
Personal Info |
Papers |
Teaching |
Links |
Generation of Basic Semi-algebraic Invariants Using Convex Polyhedra
Roberto Bagnara
Dipartimento di Matematica e Informatica
Università di Parma
Parco Area delle Scienze 53/A
I-43124 Parma
Italy
Enric Rodriguez-Carbonell
Software Department
Technical University of Catalonia
E-08034 Barcelona
Spain
Enea Zaffanella
Dipartimento di Matematica e Informatica
Università di Parma
Parco Area delle Scienze 53/A
I-43124 Parma
Italy
Abstract
A technique for generating invariant polynomial inequalities of bounded degree is presented using the abstract interpretation framework. It is based on overapproximating basic semi-algebraic sets, i.e., sets defined by conjunctions of polynomial inequalities, by means of convex polyhedra. While improving on the existing methods for generating invariant polynomial equalities, since polynomial inequalities are allowed in the guards of the transition system, the approach does not suffer from the prohibitive complexity of the methods based on quantifier-elimination. The application of our implementation to benchmark programs shows that the method produces non-trivial invariants in reasonable time. In some cases the generated invariants are essential to verify safety properties that cannot be proved with classical linear invariants.
Available: PDF, 300 DPI, 600 DPI, and 1200 DPI PostScript, DVI, BibTeX entry.
[Page last updated on August 24, 2005, 11:11:32.]
bagnara@cs.unipr.it
Home | Personal | Papers | Teaching | Links