科研之友
微信
新浪微博
Facebook
分享链接
摘要
秩函数法作为循环程序终止性分析的主流方法已经得到了深入的研究，但是现有的秩函数方法大多局限于线性或多项式秩函数的求解。针对循环程序若不存在对应的线性或多项式秩函数，现有的秩函数方法就无法证明终止性的问题，提出了一个新的方法合成给定循环程序对应的界函数。对于给定循环程序，倘若能找到其界函数，则表明该循环程序是可终止的。首先将界函数的求解问题转化为一个线性二分类问题，并选定界函数模板，根据模板建立映射关系构建训练集；然后利用所得训练集通过支持向量机（SVM）获取分类超平面进而求解出模板系数，得到候选的界函数；最后利用现有的符号验证工具redlog对该候选界函数进行验证。实验结果表明，对比于现有的秩函数方法，不仅能够应用于更多的循环程序，而且所得界函数在形式上相对于秩函数更加简化，具体为，对于某些没有线性秩函数的循环，该方法可以得到其对应的线性界函数；同时，对于某些只有多阶段线性秩函数的循环，该方法可以求解得到全局的线性界函数。
- 单位
