Program Verification by Reduction to Semi-algebraic Systems Solving

The discovery of invariants and ranking functions plays a central role in program verification. In our previous work, we investigated invariant generation and non-linear ranking function discovering of polynomial programs by reduction to semi-algebraic systems solving. In this paper we will first summarize our results on the two topics and then show how to generalize the approach to discovering more expressive invariants and ranking functions, and applying to more general programs. ? Springer-Verlag Berlin Heidelberg 2008.EICPCI-S(ISTP)