基于QBF的循环不变式构造技术

• 作者: 李舟军 陈石坤
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: 程序验证 循环不变式 带量词的布尔公式
• 年，卷（期）: 2010,（9）
• 页码范围: 76-80
• 分类号: TP311.5
• 字数: 6169字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2010.09.021

摘要

构造循环不变式是程序验证的核心问题之一.主流的循环不变式构造方法通常假设程序中的变量在无限数域上取值,然而程序执行过程中变量都是用有限长度的位向量来表示,无限数域上的循环不变式在有限数域的程序中可能不再是不变式,反之亦然.针对这一问题,本文给出一种基于QBF求解的构造有限数域上循环不变式的方法.该方法可用于构造类型丰富的不变式,包括线性(或多项式)等式(或不等式)不变式,支持加、减、乘、除、移位、位操作等,允许不变式中出现量词.本文也例证了该方法在程序终止性证明、循环上界分析、程序正确性证明等方面的应用价值.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李舟军	北京航空航天大学计算机学院	136	2221	23.0	43.0
2	陈石坤	国防科学技术大学计算机学院	3	11	1.0	3.0