Generating polynomial invariants with DISCOVERER and QEPCAD

Abstract. This paper investigates how to apply the techniques on solving semi-algebraic systems to invariant generation of polynomial programs.By our approach, the generated invariants represented as a semi-algebraic sys-tem aremore expressive than those generated with the well-established ap-proaches in the literature, which are normally represented as a conjunction of polynomial equations. We implement this approach with the computer algebra toolsDISCOVERERandQEPCAD1.Wealso explain, through the complexity analysis, why our approach is more efficient and practical than the one of [17] which directly applies first-order quantifier elimination