Automatic Discovery of Non-Linear Ranking Functions of Loop Programs

摘要：

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.

关键词： Program Verification Non-Linear Loop Ranking Function Inequality Proving BOTTEMA

作者: Yi Li

会议类型: 国际会议

会议名称: 2009 2nd IEEE International Conference on Computer Science and Information Technology(第二届计算机科学与信息技术国际会议 ICCSIT2009)

会议地点: 北京

会议语种:英文

页码: 402-406

在线出版日期: 2009-08-08（万方平台首次上网日期，不代表论文的发表时间）