基于程序骨架的软件模型验证加速方法

摘要

模型验证作为一种形式化技术,已逐渐应用于软件系统可靠性验证.但对结构复杂的大规模软件的验证,由于状态空间爆炸往往会导致验证过程效率低甚至失败.本文针对ANSI-C软件程序的性质(正确性)验证问题,提出一种基于程序骨架的模型验证加速方法.该方法首先根据性质对源程序进行剪枝,并按照最大强连通分支压缩循环路径以抽取程序骨架,采用Hoare逻辑获取循环压缩节点的不变式,显著减小路径编码长度,将待验证性质转化为SMT一阶谓词逻辑公式,并采用SMT求解器Z3进行验证.实验结果表明抽取程序骨架后的验证效率有较大提升.