通过结合迭代特化与插值进行程序验证

我们提出了一种结合迭代特化 (Iterated Specialization) 与插值 Horn 子句求解的程序安全性验证技术。我们的新方法通过利用验证问题的通用 Horn 子句表示，以模块化方式将这两种技术组合在一起。迭代特化验证器使用保持展开/折叠等价性的变换规则来转换初始的一组验证条件。在变换过程中，通过应用加宽算子来发现程序不变量。然后，利用插值 Horn 子句求解器分析输出的特化验证条件集，从而在加宽效果的基础上增加了插值效果。特化阶段和插值阶段可以迭代进行，也可以与其他改变约束传播方向（从程序前置条件向前或从错误条件向后）的变换相结合。我们通过将 VeriMAP 验证器与基于迭代特化和插值的 FTCLP Horn 子句求解器集成，实现了我们的验证技术。实验结果表明，集成后的验证器提高了各组件单独运行时的精度。