Programming a symbolic model checker in a fully expansive theorem prover

Abstract

Model checking and theorem proving are two complementary approaches to formal verification. In this paper we show how binary decision diagram (BDD) based symbolic model checking algorithms may be embedded in a theorem prover to take advantage of the comparatively secure environment without incurring an unacceptable performance penalty. © Springer-Verlag Berlin Heidelberg 2003.