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.