Randomized backtracking in state space traversal

Abstract

While exhaustive state space traversal is not feasible in reasonable time for complex concurrent programs, many techniques for efficient detection of concurrency errors and testing of concurrent programs have been introduced in recent years, such as directed search and context-bounded model checking. We propose to use depth-first traversal with randomized backtracking, where it is possible to backtrack from a state before all outgoing transitions have been explored, and the whole process is driven by random number choices. Experiments with a prototype implementation in JPF on several Java programs show that, in most cases, fewer states must be explored to find an error with our approach than using the existing techniques. © 2011 Springer-Verlag.