13.10.2005

Selective Search in Bounded Model Checking of Reachability Properties

Bounded Model Checking (BMC) encodes a model checking problem in the propositional logic. Diagnosing the resulting formula as satisfiable provides a counterexample. While surprisingly efficient for many complex systems, in general BMC still fails to be complete and is a method of falsification rather then validation. The major obstacle is satisfiability testing (SAT). The talk introduces a selective search to the standard DLL SAT algorithm, allowing to profit from several optimization techniques proposed for non-symbolic methods. Partial-order reductions are shown as an example of selective search. Preliminary experimental results confirm that the selective search can significantly improve the effectiveness of BMC.