Generation of basic semi-algebraic invariants using convex polyhedra

Abstract. A technique for generating invariant polynomial inequalities of bounded degree is presented using the abstract interpretation frame-work. It is based on overapproximating basic semi-algebraic sets, i.e., sets de ned by conjunctions of polynomial inequalities, by means of convex polyhedra. While improving on the existing methods for generating in-variant polynomial equalities, since polynomial inequalities are allowed in the guards of the transition system, the approach does not suer from the prohibitive complexity of the methods based on quantier-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 proper-ties that cannot be proved with classical linear invariants.