Sciweavers

BIRTHDAY
2007
Springer

Generating Polynomial Invariants with DISCOVERER and QEPCAD

14 years 5 months ago
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
Yinghua Chen, Bican Xia, Lu Yang, Naijun Zhan
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where BIRTHDAY
Authors Yinghua Chen, Bican Xia, Lu Yang, Naijun Zhan
Comments (0)