计算机应用

作者：谭旺, 李轶

单位：1.中国科学院 重庆绿色智能技术研究院, 重庆 400714；2.中国科学院大学 计算机科学与技术学院, 北京 101408

关键词：程序验证,循环程序终止性,支持向量机,界函数,秩函数

基金：国家自然科学基金资助项目(11771421);中国科学院“西部之光”;国家重点研发计划项目(2020YFA07123000);重庆市自然科学基金资助项目(cstc2019jcyj-msxmX0638)

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

来源：2022年第2期

《计算机应用》期刊编辑部

查看计算机应用杂志2022年第2期