Random Search: It non-deterministically selects a state on the frontier to explore, and can find results even when exhaustive search is not feasible. Its success in artificial intelligence makes it a good candidate search strategy for model checking, but its application obviously limits the rigor of verification, because faults can hide in portions of the state space not explored in random trials. Random search should be used when the objective is more bug-finding than verification. For high-assurance systems, its usage is recommended earlier in the development and debugging when the number of logical faults is higher than in the later stages and when their removal is the most cost effective.
We experimented with using a purely random search to find a known bug in DEOS using JPF; however, the counterexample was considerably longer and took more time and memory to produce than with using the coverage heuristics. The LURCH system employs random search and has performed well in certain cases.