Depth Bounded Explicit State Model Checking

We present algorithms to efficiently bound the depth of the state spaces explored by explicit state model checkers. Given a parameter k, our algorithms guarantee finding any violation of an invariant that is witnessed using a counterexample of length k or less from the initial state. Though depth bounding is natural with breadth first search, explicit state model checkers are unable to use breadth first search due to prohibitive space requirements, and use depth first search to explore large state spaces. Thus, we explore efficient ways to perform depth bounding with depth first search. We prove our algorithms sound (in the sense that they explore exactly all the states reachable within a depth bound), and show their effectiveness on large real-life models from Microsoft’s product groups.