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 dened by conjunctions of polynomial inequalities, by means of con-vex 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 suer from the prohibitive complexity of 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 just classical linear invariants.