...
We gave an overview of SAT-based model checking checking, starting from bounded model checking
and a small examples for bit-blasting. We discussed safety, liveness and fairness checking, before
turning towards completeness issues. We looked at complete algorithm, including k-induction, its
incremental implementation, deductive model checking, interpolants for model checking, and finally
at a simplified version of property driven reachability.
...