Interleaved Invariant Checking with Dynamic Abstraction
Liang Zhang, Mukul R. Prasad, Michael S. Hsiao · Lecture notes in computer science · 2005
The notion of dynamic abstraction was recently introduced as a means of abstracting a model during the process of model checking. In this paper we show, theoretically and practically, how dynamic abstraction can be used with different algorithms for invariant checking, namely forward, backward and interleaved state-space traversal. Further, we formalize the correctness guarantees that can be made under different invariant checking algorithms operating on a dynamically abstracted model. We report experimental results on industrial strength benchmarks to further demonstrate the power and versatility of this abstraction mechanism in conjuction with interleaved state-space traversal. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.