Automatic discovery of non-linear ranking functions of loop programs

Author

Li, Yi

Author_Institution

Chengdu Inst. of Comput. Applic., Chinese Acad. of Sci., Chengdu, China

fYear

2009

fDate

8-11 Aug. 2009

Firstpage

402

Lastpage

406

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;

fLanguage

English

Publisher

ieee

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

Type

conf

DOI

10.1109/ICCSIT.2009.5234919

Filename

5234919

Link To Document

https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=3318452