SAT-based Model-Checking

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.

Armin Biere, Johannes Kepler University, Linz, Austria

put your bio here