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.

• Type: Conference
• Year: 2003
• Where: TPHOL
• Authors: Hasan Amjad
• Keywords: Artificial Intelligence, Model Checking, Model Checking Algorithms, Theorem Proving, TPHOL 2003