Two well-known approaches to the verification of reactive systems are deductive verification and model checking. After briefly reviewing them, we present deductive model checking, which combines these two approaches. The new procedure uses deduction to extend the classical tableau-based model checking algorithms to the case of infinite-state systems.
Appeared in Logic, Language and Computation, CSLI, 1997.
Postscript, PDF. © 1997, CSLI.