Sciweavers

Share
CAV
2000
Springer

Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking

8 years 12 months ago
Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking
In this paper we show how to do symbolic model checking using Boolean Expression Diagrams (BEDs), a non-canonical representation for Boolean formulas, instead of Binary Decision Diagrams (BDDs), the traditionally used canonical representation. The method is based on standard fixed point algorithms, combined with BDDs and SAT-solvers to perform satisfiability checking. As a result we are able to model check systems for which standard BDD-based methods fail. For example, we model check a liveness property of a 256 bit shift-and-add multiplier and we are able to find a previously undetected bug in the specification of a 16 bit multiplier. As opposed to Bounded Model Checking (BMC) our method is complete in practice. Our technique is based on a quantification procedure that allows us to eliminate quantifiers in Quantified Boolean Formulas (QBF). The basic step of this procedure is the up-one operation for BEDs. In addition we list a number of important optimizations to reduce the number of...
Poul Frederick Williams, Armin Biere, Edmund M. Cl
Added 24 Aug 2010
Updated 24 Aug 2010
Type Conference
Year 2000
Where CAV
Authors Poul Frederick Williams, Armin Biere, Edmund M. Clarke, Anubhav Gupta
Comments (0)
books