Generating Counter-Examples Through Randomized Guided Search

Abstract. 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 lowcost 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 r...

• Type: Conference
• Year: 2007
• Where: SPIN
• Authors: Neha Rungta, Eric G. Mercer
• Keywords: Model Checking, Randomized Depth-first Search, Randomized Guided Search, SPIN 2007, Theoretical Computer Science