Computational resources are increasing rapidly with the explosion of multi-core processors readily available from major vendors. Model checking needs to harness these resources to help make it more effective in practical verification. Directed model checking uses heuristics in a guided search to rank states in order of interest. Randomizing guided search makes it possible to harness computation nodes by running independent searches in parallel in a effort to discover counter-examples to correctness. Initial attempts at adding randomization to guided search have achieved very limited success. In this work, we present a new low-cost randomized guided search technique that shuffles states in the priority queue with equivalent heuristic ties. We show in an empirical study that randomized guided search, overall, decreases the number of states generated before error discovery when compared to a guided search using the same heuristic. To further evaluate the performance gains of randomized guided search using a particular heuristic, we compare it with randomized depth-first search. Randomized depth-first search shuffles transitions and generally improves error discovery over the default transition order implemented by the model checker. In the context of evaluating randomized guided search, a randomized depth-first search provides a lower bound for establishing performance gains in directed model checking. In the empirical study, we show that with the correct heuristic, randomized guided search outperforms randomized depth-first search both in effectively finding counter-examples and generating shorter counter-examples.

Pdf version

Conference Slides

N. Rungta and E. G. Mercer. “Generating Counter-examples through Randomized Guided Search,” SPIN Workshop on Model Checking of Software, Berlin, Germany, July 2007.

 @InProceedings{rungta:spin07,
 author =   {N. Rungta and E.~G.~Mercer},
 title =   {Generating Counter-Examples Through Randomized Guided Search},
 booktitle =  {Proceedings of the 14th International SPIN Workshop on Model Checking of Software},
 year =  {2007},
 address =  {Berlin, Germany},
 month =  {July},
 OPTorganization = {},
 publisher =  {Springer--Verlag},
 OPTnote =   {},
 pages = {39-57},
 }