基于不变式生成的循环停机性验证

• 作者: 李梦君 李舟军 邢建英
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: 不变式 停机性验证 最优化问题 复杂度上界
• 年，卷（期）: 2012,（4）
• 所属期刊栏目: 软件工程
• 页码范围: 108-113
• 分类号: TP301
• 字数: 4978字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2012.04.021

摘要

循环的停机性验证是程序验证中的一个难点.程序不变式用来描述程序变量的取值关系,其中线性不变式可以帮助描述程序变量间的线性关系,循环不变式能够有效刻画循环中的变量关系.本文基于线性不变式和多项式循环不变式的生成,将循环的停机性验证转化为求解一个最优化问题,给出了一个实用的程序停机性验证框架.基于该框架可以自动地验证程序的停机性,并给出循环的复杂度上界.实验结果说明了该方法的实用性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李舟军	国防科学技术大学计算机学院	17	339	7.0	17.0
2	李梦君	国防科学技术大学计算机学院	16	294	7.0	16.0
3	邢建英	国防科学技术大学计算机学院	3	14	2.0	3.0