×

zbMATH — the first resource for mathematics

Integrating BDD-based and SAT-based symbolic model checking. (English) Zbl 1057.68623
Armando, Alessandro (ed.), Frontiers of combining systems. 4th international workshop, FroCos 2002, Santa Margherita Ligure, Italy, April 8–10, 2002. Proceedings. Berlin: Springer (ISBN 3-540-43381-3). Lect. Notes Comput. Sci. 2309, 49-56 (2002).
Summary: Symbolic model checking is a very successful formal verification technique, classically based on Binary Decision Diagrams (BDDs). Recently, propositional satisfiability (SAT) techniques have been proposed as a computational basis for symbolic model checking, and proved to be an effective alternative to BDD-based techniques. In this paper we show how BDD-based and SAT-based techniques have been effectively integrated within the NuSMV symbolic model checker.
For the entire collection see [Zbl 0990.00065].

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68W30 Symbolic computation and algebraic computation
Software:
Chaff; CUDD; NuSMV; SPIN
PDF BibTeX XML Cite
Full Text: Link