In this talk, I will discuss McMillan’s algorithm for fully SAT-based unbounded symbolic model checking. The method is based on computing Craig interpolants. In terms of performance, the algorithm is substantially more efficient than BDD-based model checking. I will also explain how we modify McMillan’s algorithm to analyze the backward reachability of initial states from final states in a transition system.