Hybrid BDD and All-SAT Method for Model Checking

We present a new hybrid BDD and SAT-based algorithm for model checking. Our algorithm is based on backward search, where each pre-image computation consists of an efficient All-SAT procedure. The All-SAT procedure exploits a graph representation of the model to dynamically prune the search space, thus preventing unnecessary search in large sub-spaces, and for identifying independent sub-problems. Apart from the SAT mechanisms, BDD structures are used for storing the input to, and output of the pre-image computation. In this way, our hybrid approach enjoys the benefits of both worlds: on the one hand, basing the pre-image computation on SAT technology avoids expensive BDD quantification operations and the corresponding state space blow up. On the other hand, our model checking framework still enjoys the advantages of symbolic space reduction in holding intermediate images. Furthermore, our All-SAT analyzes the model and avoids redundant exploration of sub-spaces that are completely f...

• Type: Conference
• Year: 2009
• Where: BIRTHDAY
• Authors: Avi Yadgar, Orna Grumberg, Assaf Schuster
• Keywords: All-SAT Procedure, Applied Computing, BIRTHDAY 2009, Model Checking, Pre-image Computation