Property-directed incremental invariant generation
Property-directed incremental invariant generation
复制标题
DOI：
10.1007/s00165-008-0080-9
复制
发表时间：
2008-07-01
影响因子：
1
通讯作者：
Manna, Zohar
中科院分区：
文献类型：
--
作者：
Bradley, Aaron R.;Manna, Zohar
分析系统（如程序或电路）的一种基本方法是不变性分析，在这种方法中，人们证明一个断言对所有可到达的状态都成立。通常，证明是通过归纳法进行的；然而，一个断言虽然是不变的，但可能不是归纳的（可以通过归纳证明）。不变量生成过程构造辅助归纳断言，以加强断言的归纳性。我们描述了一种生成增量和属性导向不变量的一般方法。我们的方法不是生成一个大型的辅助归纳断言，而是生成许多简单的断言，每个断言相对于之前生成的断言都是归纳的。增量生成适用于并行化。我们的方法也是面向属性的，因为它生成与增强给定断言相关的归纳断言。我们描述了我们的方法的两个实例：一个生成有限状态系统的子句不变量的过程和一个生成数值无限状态系统的仿射不等式的过程。我们提供的证据表明，我们的方法适用于检查一些大型有限状态系统的安全性质。
A fundamental method of analyzing a system such as a program or a circuit is invariance analysis, in which one proves that an assertion holds on all reachable states. Typically, the proof is performed via induction; however, an assertion, while invariant, may not be inductive (provable via induction). Invariant generation procedures construct auxiliary inductive assertions for strengthening the assertion to be inductive. We describe a general method of generating invariants that is incremental and property-directed. Rather than generating one large auxiliary inductive assertion, our method generates many simple assertions, each of which is inductive relative to those generated before it. Incremental generation is amenable to parallelization. Our method is also property-directed in that it generates inductive assertions that are relevant for strengthening the given assertion. We describe two instances of our method: a procedure for generating clausal invariants of finite-state systems and a procedure for generating affine inequalities of numerical infinite-state systems. We provide evidence that our method scales to checking safety properties of some large finite-state systems.