@inproceedings{andrajamani2011depth,
author = { and Rajamani, Sriram},
title = {Depth bounded explicit-state model checking},
booktitle = {Proceedings of the 18th international SPIN conference on Model checking software},
year = {2011},
month = {July},
abstract = {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.},
publisher = {Springer-Verlag},
url = {http://approjects.co.za/?big=en-us/research/publication/depth-bounded-explicit-state-model-checking-2/},
pages = {57-74},
isbn = {978-3-642-22305-1},
edition = {Proceedings of the 18th international SPIN conference on Model checking software},
}