Survey on Directed Model Checking

This paper surveys and gives historical accounts to the algorithmic essentials of directed model checking, a promising bug-hunting technique to mitigate the state explosion problem. In the enumeration process, successor selection is prioritized. The authors discuss existing guidance and methods to automatically generate them by exploiting system abstractions. They extend the algorithms to feature partial-order reduction and show how liveness problems can be adapted by lifting the search space. For deterministic, finite domains they instantiate the algorithms to directed symbolic, external and distributed search.