## 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 and general framework that can be used
to integrate a diverse number
of other verification tools.

In *8th International Conference on Computer-Aided Verification*,
LNCS vol. 1102, pp. 209-219, Springer-Verlag, July 1996.

Postscript,
PDF.
© 1996, Springer Verlag.

© Henny Sipma /
sipma@cs.stanford.edu
Last modified: Thu Mar 29 18:11:29 PST 2001