Due to determining the classical ranking functions of program verification, a new approach was proposed based on the theory of semi-algebraic systems. It automatically converts the problem of program verification to solve the ranking function of semi-algebraic systems. The sufficient and necessary conditions on parameters in ranking functions can be obtained using symbolic computation tool, DISCOVERER and Farkas' Lemma, and then automatically synthesized the novel ranking function by symbolic computations. The method with other methods to do a comparative is reasonable theoretically, and experimental results show that it is efficient.
