On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction
On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction
复制标题
结合静态分析、定理证明和抽象来证明安全性
DOI：
--
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
Eli Singerman
中科院分区：
文献类型：
--
作者：
Vlad Rusu;Eli Singerman
我们提出了一种基于静态分析，定理证明和抽象技术之间的紧密相互作用的新方法来证明反应性系统的安全性能。该方法会逐步构建证明或找到反例。每个步骤都包括应用其中一种技术，并在上一步中从失败中获得的信息进行建设性使用。用户干预的量受到限制，并且在每个步骤中都受到系统的高度指导。我们在三个简单示例上演示了该方法，并证明，通过使用它可以证明其属性比将每个组件用作独立的属性更多。
We present a new approach for proving safety properties of reactive systems, based on tight interaction between static analysis, theorem proving and abstraction techniques. The method incrementally constructs a proof or finds a counterexample. Every step consists of applying one of the techniques and makes constructive use of information obtained from failures in previous steps. The amount of user intervention is limited and is highly guided by the system at each step. We demonstrate the method on three simple examples, and show that by using it one can prove more properties than by using each component as a stand-alone.