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

作     者：陈石坤 李舟军 CHEN Shi-kun;LI Zhou-jun

作者机构：国防科学技术大学计算机学院湖南长沙410073 北京航空航天大学计算机学院北京100191 

出 版 物：《计算机工程与科学》 (Computer Engineering & Science)

年 卷 期：2010年第32卷第9期

页      面：76-80页

核心收录：

学科分类：08[工学] 0835[工学-软件工程] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：国家自然科学基金资助项目(60703075 90718017) 教育部高等学校博士学科点专项基金资助项目(20070006055) 

主　　题：程序验证 循环不变式 带量词的布尔公式 

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