Heuristic Search: Heuristic search exploits the information known about the system under analysis in order to accelerate the search process. The basic idea of heuristic search is that rather than trying all the possible search paths, the model checker tries to focus on paths that seem to be getting it nearer to the error states. This is a strong motivation for the use of heuristic search in bug finding; model checkers which rely on traditional DFS algorithms tend to return much longer counterexamples than those which support heuristic search. Of course, the model checker which uses heuristic search generally can’t be sure that it is really close to an error state, but it might be able to have a good guess. Heuristics are used to help the model checker make that guess. Different search algorithms can be combined with heuristics. To use heuristic search, we need an evaluation function that scores a state in the state space according to how close to the error state it seems to be—the higher the score, the more desirable the state is to be explored next.