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 semialgebraic system are more expressive than those generated with the wellestablished approaches in the literature, which are normally represented as a conjunction of polynomial equations. We implement this approach with the computer algebra tools DISCOVERER and QEPCAD1 . We also 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. keywords Program Verification, Invariant Generation, Polynomial Programs, Semi-Algebraic Systems; Quantifier Elimination, DISCOVERER, QEPCAD

• Type: Conference
• Year: 2007
• Where: BIRTHDAY
• Authors: Yinghua Chen, Bican Xia, Lu Yang, Naijun Zhan
• Keywords: Applied Computing, BIRTHDAY 2007, Invariant Generation, Polynomial Programs, Semi-algebraic Systems