Vlad Rusu and Eli Singerman. On Proving Safety Properties by Integrating
Static Analysis, Theorem Proving and Abstraction. To appear in Tools and Algorithms for the Construction and Analysis of Systems (TACAS'99), Amsterdam (Netherlands), LNCS.
Abstract
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.
Full postscript text.