Title :
Automatic discovery of non-linear ranking functions of loop programs
Author_Institution :
Chengdu Inst. of Comput. Applic., Chinese Acad. of Sci., Chengdu, China
Abstract :
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.
Keywords :
program control structures; program verification; automated program verification; inequality prover BOTTEMA; loop programs; nonlinear ranking function; region-based search; Computer applications; Embedded software; Embedded system; Lagrangian functions; Linear programming; Polynomials; Software safety; State-space methods; Sufficient conditions; BOTTEMA; Inequality Proving; Non-Linear Loop; Program Verification; Ranking Function;
Conference_Titel :
Computer Science and Information Technology, 2009. ICCSIT 2009. 2nd IEEE International Conference on
Conference_Location :
Beijing
Print_ISBN :
978-1-4244-4519-6
Electronic_ISBN :
978-1-4244-4520-2
DOI :
10.1109/ICCSIT.2009.5234919
