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

that remain unchanged by further executions of the program. However, in order
to guarantee termination, the method introduces imprecision by use of an ex-
trapolation operator called widening/narrowing . This operator often causes the
technique to produce weak invariants. Moreover, proposing widening/narrowing
operators with certain concerns of completeness is not easy and becomes a key
challenge for abstract interpretation based techniques [7,1].
In contrast, [19,20,22,23,24] exploited the theory of polynomial algebra to
discover invariants of polynomial programs. [19] applied the technique of linear
algebra to generate polynomial equations of bounded degree as invariants of pro-
grams with ane assignments. [22,23] first proved that the set of polynomials
serving as loop invariants has the algebraic structure of an ideal, then proposed
an invariant generation algorithm by using fixpoint computation, and finally
implemented the algorithm by the Grobner bases and the elimination theory.
The approach is theoretically sound and complete in the sense that if there is
an invariant of the loop that can be expressed as a conjunction of polynomial
equations, applying the approach can indeed generate it. [24] presented a similar
approach to finding polynomial equation invariants whose form is priori deter-
mined (called templates) by using an extended Grobner basis algorithm over
templates.
Compared with the polynomial algebraic approaches that can only gener-
ate invariants represented as polynomial equations, [5] proposed an approach to
generate linear inequalities as invariants for linear programs, based on Farkas'
Lemma and non-linear constraint solving. In addition, [17] proposed a very gen-
eral approach for automatic generation of more expressive invariants by exploit-
ing the technique of quantifier elimination, and applied the approach to Pres-
burger Arithmetic and quantifier-free theory of conjunctively closed polynomial
equations. Theoretically speaking, the approach can also be applied to the the-
ory of real closed fields, but [17] pointed out that this is impractical in reality
because of the high complexity of quantifier elimination, which is double expo-
nential [8]. To handle the problem, [6] exploited the techniques of parametric
abstraction, Lagrangian relaxation and semidefinite programming to generate
invariants as well as ranking functions of polynomial programs. Compared with
the approach of [17], [6]'s is more ecient, as first-order quantifier elimination
is not directly applied there. However, [6]'s approach is incomplete in the sense
that, for some program that may have ranking functions and invariants of the
predefined form, applying the approach may not be able to find them, as La-
grangian relaxation and over-approximation of the positive semi-definiteness of
a polynomial are used.
In this paper, we attack the problem raised in [17] on how to eciently gen-
erate polynomial invariants of programs over real closed fields and present a
more practical and ecient approach to it by exploiting our results on solving
semi-algebraic systems (SASs). The outline of our approach is as follows: we first
reduce polynomial invariant generation problem to solving semi-algebraic sys-
tems; then apply our theories and tools on solving SASs, in particular, on root
classification of parametric SASs [30,31,32] and real root isolation of constant