Sciweavers

Share
TPHOL
2003
IEEE

Programming a Symbolic Model Checker in a Fully Expansive Theorem Prover

10 years 3 months ago
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.
Hasan Amjad
Added 05 Jul 2010
Updated 05 Jul 2010
Type Conference
Year 2003
Where TPHOL
Authors Hasan Amjad
Comments (0)
books