Hits:

Indexed by:会议论文

Date of Publication:2013-10-29

Page Number:736-740

Key Words:模型检测;程序骨架;路径压缩;程序验证

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