Under-approximation Heuristics for Grid-based Bounded Model Checking

In this paper, we consider the effect of BDD-based under-approximation on a hybrid approach using BDDs and SAT-BMC for error detection on a computing grid. We experimentally study effect of under-approximation approaches on a non-traditional parallelization of BMC based on state space partitioning. This parallelization is accomplished by executing multiple instances of BMC independently from different seed states, that are selected from the reachable states in different partitions. Such states are spread out across the state space and can potentially be deep. Since all processors work independently of each other, this scheme is suitable for bug hunting using a grid-like network. Our experimental results demonstrate improvement over existing approaches, and we show that the method can effectively utilize a large grid network.