基于SVM的多项式循环程序秩函数生成

来源：软件学报杂志2019年第7期北京时间：

作者：李轶,蔡天训,樊建峰,吴文渊,冯勇

单位：李轶，中国科学院 重庆绿色智能技术研究院 自动推理与认知重庆市重点实验室, 重庆 40071411,蔡天训，萨基姆通讯(深圳)有限公司, 广东 深圳 51800002,樊建峰，中国科学院 重庆绿色智能技术研究院 自动推理与认知重庆市重点实验室, 重庆 400714;中国科学院大学 计算机科学与技术学院, 北京 10009303,吴文渊，中国科学院 重庆绿色智能技术研究院 自动推理与认知重庆市重点实验室, 重庆 40071404,冯勇，中国科学院 重庆绿色智能技术研究院 自动推理与认知重庆市重点实验室, 重庆 40071405

摘要：程序终止性问题是自动程序验证领域中的一个研究热点.秩函数探测是进行终止性分析的主要方法.针对单重无条件分支的多项式循环程序，将其秩函数计算问题归结为二分类问题，从而可利用支持向量机（SVM）算法来计算程序的秩函数.与基于量词消去技术的秩函数计算方法不同，该方法能在可接受的时间范围内探测到更为复杂的秩函数.

关键词：程序终止性;SVM;机器学习;秩函数

基金资助：国家自然科学基金（61572024，61103110，11471307）