A* Search: A* (pronounced “A star”) is a best-first search that attempts to minimize the total length of the path from the initial state to the goal state. It combines advantages of breadth-first search, where the shortest path is found first, with those of best-first search, where the state that we guess is closest to the goal state is explored next.
The heuristic function score, f(s), for a state s is calculated as the sum of the length of the path so far, g(s), plus the estimated length to the goal state, h(s):
f(s) = g(s) + h(s)
This search strategy is particularly attractive for verification purposes where we want to get the shortest error trace to a bug. We may often use other simple-minded search strategies to find a bug, but then use A* to get the shortest path to it.