Model Checking and Deduction for Verifying Infinite-state Systems

Henny Sipma, Tomas Uribe, Zohar Manna

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.

© Henny Sipma /
Last modified: Thu Mar 29 17:58:17 PST 2001