Program verification by using DISCOVERER

Abstract. Recent advances in program verification indicate that vari-ous verification problems can be reduced to semi-algebraic system (SAS for short) solving. An SAS consists of polynomial equations and poly-nomial inequalities. Algorithms for quantifier elimination of real closed fields are the general method for those problems. But the general method usually has low efficiency for specific problems. To overcome the bot-tleneck of program verification with a symbolic approach, one has to combine special techniques with the general method. Based on the work of complete discrimination systems of polynomials [33, 31], we invented new theories and algorithms [32, 30, 35] for SAS solving and partly im-plemented them as a real symbolic computation tool in Maple named DISCOVERER. In this paper, we first summarize the results that we have done so far both on SAS-solving and program verification with DISCOVERER, and then discuss the future work in this direction, in-cluding SAS-solving itself, termination analysis and invariant generation of programs, and reachability computation of hybrid systems etc.