Automatic discovery of non-linear ranking functions of loop programs

Automatic discovery of non-linear ranking functions of loop programs
复制标题

DOI：
10.1109/iccsit.2009.5234919
复制
发表时间：
2009-09
期刊：
2009 2nd IEEE International Conference on Computer Science and Information Technology
影响因子：
--
通讯作者：
Yi Li
Yi Li
中科院分区：
其他
文献类型：
--
作者：
Yi Li

文献摘要

被引文献

相似文献

本文提出了一种程序循环的非线性排序函数的综合方法。在基于区域搜索的基础上，将非线性排序函数的发现归结为不等式检验。然后，不等式证明器BOTTEMA可以用来检查不等式的有效性。与其他方法相比，由于BOTTEMA的独特性，新方法还可以发现带有偏旁部首的排序函数。几个有趣的例子来说明我们的技术。
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.