Automatic Synthesis of Linear Program Ranking Functions
Xiaolin Qin · Journal of Sichuan University · 2009
To determine the classical ranking functions of program verification,a new approach was proposed based on the theory of semi-algebraic systems.It automatically converted the problem of program verification to solve the ranking function of semi-algebraic systems.The sufficient and necessary conditions of parameters in ranking functions could be obtained using symbolic computation tool,DISCOVERER and Farkas' Lemma,and then the novel ranking function was automatically synthesized by symbolic computations.The comparision with other methods and experimental results showed that this method was efficient.