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 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 just classical linear invariants.
CitationBagnara, R., Rodríguez, E., Zaffanella, E. "Generation of basic semi-algebraic invariants using convex polyhedra". 2005.
All rights reserved. This work is protected by the corresponding intellectual and industrial property rights. Without prejudice to any existing legal exemptions, reproduction, distribution, public communication or transformation of this work are prohibited without permission of the copyright holder. If you wish to make any use of the work not provided for in the law, please contact: email@example.com