危险不变量

静态分析器搜索被称为安全不变量的安全性过近似证明。从根本上说，此类分析器将轨迹总结为状态集合，从而以区分轨迹的能力换取计算可处理性。相反，静态缺陷查找器（例如有界模型检测）以反例形式提供断言失败的证据，可供用户检查。然而，当分析需要循环多次迭代才能暴露缺陷的程序时，静态缺陷查找器因计算量随缺陷深度指数增长而难以扩展。我们提出一种寻找缺陷的新方法，其兼具抽象解释的性能与BMC的具体精度。为此，我们引入危险不变量的概念——安全不变量的对偶。危险不变量总结保证到达错误状态的轨迹集合。这种总结使我们能够在不产生误报且无需显式展开循环的情况下找到深层缺陷。我们给出危险不变量的二阶公式，并利用先前工作中描述的二阶SAT求解器计算文献中复杂程序的危险不变量。