Search algorithms for automated validation

A novel search technique called highway search is introduced. The search technique relies on a highway simulation which takes several homogeneous walks through a (possibly infinite) state space. Furthermore, we provide a memory-efficient algorithm that approximates a highway search and we prove that, under particular conditions, they coincide. The effectiveness of highway search is compared to two mainstream search techniques, viz. random search and randomised depth-first search. Our results demonstrate that randomised depth-first search explores the least amount of states in the effort of finding states of interest, whereas a highways search yields the shortest witnessing traces to such states.