Generating Polynomial Invariants with DISCOVERER and QEPCAD - Formal Methods and Hybrid Real-Time Systems - page 67

Generating Polynomial Invariants with
DISCOVERER and QEPCAD

Yinghua Chen 1 ,BicanXia 1 ,LuYang 2 , and Naijun Zhan 3 ,

1 LMAM & School of Mathematical Sciences, Peking University
2 Institute of Theoretical Computing, East China Normal University
3 Lab. of Computer Science, Institute of Software, Chinese Academy of Sciences
South Fourth Street, No. 4, Zhong Guan Cun, Beijing, 100080, P.R. China
[e-mail]

Dedicated to Prof. Chaochen Zhou on his 70th Birthday

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 are more 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 tools DISCOVERER and QEPCAD 1 . We also explain, through the
complexity analysis, why our approach is more ecient 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, DISCOV-
ERER, QEPCAD.

1 Introduction

Loop invariant generation together with loop termination analysis of programs
plays a central role in program verification. Since the late sixties (or early sev-
enties) of the 20th century when the so-called Floyd-Hoare-Dijkstra inductive
assertion method, the dominant method on automatic verification of programs,
[11,14,9] was invented, there have been lots of attempts to handle the loop prob-
lems, e.g. [25,13,16,15], but only with a limited success.
Recently, due to the advance of computer algebra, several methods based on
symbolic computation have been applied successfully to invariant generation,
for example the techniques based on abstract interpretation [7,1,21,6], quantifier
elimination [5,17] and polynomial algebra [19,20,22,23,24].
The basic idea behind the abstract interpretation approaches is to perform
an approximate symbolic execution of a program until an assertion is reached

This work is supported in part by NKBRPC-2002cb312200, NKBRPC-
2004CB318003, NSFC-60493200, NSFC-60421001, NSFC-60573007, and NKBRPC-
2005CB321902.
Corresponding author.
1 http://www.cs.usna.edu/~qepcad/B/QEPCAD.html