Abstraction-guided model checking using symbolic IDA* and heuristic synthesis

Abstract

A heuristic-based symbolic model checking algorithm, BDD-IDA* that efficiently falsifies invariant properties of a system is presented. As in bounded model checking, the algorithm uses an iterative deepening search strategy. However, in our case, the search strategy is guided by a heuristic that is computed from an abstract model, which is derived from the concrete model by a synthesis technique. Synthesis involves eliminating so-called weak variables from the concrete specification, where the weak variables are identified by a data-dependency analysis. Unique to this work is the use of the depth-first IDA* search algorithm in a BDD setting, and the automatic synthesis of the heuristic. The performance of the approach on a large number of small examples is compared with standard BDD-based approaches. Experiments on a variety of real-world models from different domains are also conducted. The approach reveals a consistent improvement on all models, and in some cases a speed-up of 2 orders of magnitude is obtained. © IFIP International Federation for Information Processing 2005.