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

摘要

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