Automatic discovery of non-linear ranking functions of loop programs
Yi Li · 2009
We present a method for the synthesis of non-linear ranking function of a program loop. Based on the region-based search, it reduces the non-linear ranking function discovering to the inequality checking. The inequality prover BOTTEMA then can be utilized to check validity for inequalities. In contrast to other approaches, the new approach can also discover the ranking function with the radicals due to BOTTEMA's distinct features. Several interesting examples are given to illustrate our technique.