Incremental, Inductive Model Checking
Aaron R. Bradley · 2013
IC3, a model checking algorithm for invariance properties, has inspired a fair amount of research since it was first noticed in 2011 and is now widely used in the EDA industry. It is rooted in the deductive approach to verification, central to which is the application of mathematical induction. IC3 applies induction in two ways: in the typical manner, to detect convergence to an inductive strengthening of the property, and in an incremental manner, to discover relatively inductive lemmas in response to concrete error states. Core ideas in IC3 have been lifted to algorithms for model checking LTL and CTL properties and for analyzing infinite-state systems.