IC3 and beyond: Incremental, inductive verification

Abstract

IC3, a SAT-based safety model checking algorithm introduced in 2010 [1, 2], is considered among the best safety model checkers. This tutorial discusses its essential ideas: the use of concrete states, called counterexamples to induction, to motivate lemma discovery; the incremental application of induction to generate the lemmas; and the use of stepwise assumptions to allow dynamic shifting between inductive lemma generation and propagation of lemmas as predicates. © 2012 Springer-Verlag.