A Way of Validating Polynomial Program with Semi-algebraic System

Program checking is an interesting and challenging problem. Many kinds of programs can be formulated as polynomial programs, expressing the same meanings in a mathematical way. Moreover, with the mathematic framework of semi-algebraic systems, the polynomial based model checking can be applied directly and efficiently, as well as shows a good solution to reduce the state explosion problem. In this article, we show an easy way to translate the polynomial program into a semi-algebraic transition system, and then check the properties by computing the zeros.