## Deductive Model Checking

*Henny Sipma,
Tomas Uribe,
Zohar Manna*
We present an extension of classical tableau-based model checking
procedures to the case of infinite-state systems,
using deductive methods in an incremental construction
of the behavior graph.
Logical formulas are used to represent infinite sets of states
in an abstraction of this graph, which is repeatedly refined in
the search for a counterexample computation,
ruling out large portions of the graph before they are
expanded to the state-level.
This can lead to large savings, even in the case of finite-state systems.
Only local conditions need to be checked at each step, and previously
proven properties can be used to further constrain the search.
Although the resulting method is not always automatic,
it provides a flexible, general and complete framework that can
integrate a diverse number of other verification tools.

Appeared in *Formal Methods in System Design*, Vol 15, pp 49-74
(1999).

Postscript,
PDF.
© 1999, Kluwer Academic Publishers.

Last modified: Thu Mar 29 10:04:31 PST 2001