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

• 作者: 冯勇 吴文渊 李轶 樊建峰 蔡天训
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 程序终止性 SVM 机器学习 秩函数
• 年，卷（期）: 2019,（7）
• 所属期刊栏目: 软件形式化验证专题
• 页码范围: 1901-1915
• 页数: 15页
• 分类号: TP301
• 字数: 12420字
• 语种: 中文
• DOI: 10.13328/j.cnki.jos.005748

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李轶	中国科学院重庆绿色智能技术研究院自动推理与认知重庆市重点实验室	13	20	2.0	4.0
2	冯勇	中国科学院重庆绿色智能技术研究院自动推理与认知重庆市重点实验室	52	233	8.0	13.0
3	吴文渊	中国科学院重庆绿色智能技术研究院自动推理与认知重庆市重点实验室	19	79	6.0	8.0
4	樊建峰	中国科学院重庆绿色智能技术研究院自动推理与认知重庆市重点实验室	2	0	0.0	0.0
8	蔡天训		1	0	0.0	0.0