Title :
Incremental, Inductive Model Checking
Author :
Bradley, Aaron R.
Author_Institution :
Univ. of Colorado at Boulder, Boulder, CO, USA
Abstract :
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.
Keywords :
formal verification; systems analysis; temporal logic; CTL properties; EDA industry; IC3; LTL properties; convergence detection; deductive approach; incremental model checking; inductive lemmas; inductive model checking; infinite-state system analysis; invariance properties; mathematical induction; verification; Algorithm design and analysis; Concrete; Convergence; Games; Model checking; Safety; Standards; hardware; model checking; temporal logic; verification;
Conference_Titel :
Temporal Representation and Reasoning (TIME), 2013 20th International Symposium on
Conference_Location :
Pensacola, FL
Print_ISBN :
978-1-4799-2240-6
DOI :
10.1109/TIME.2013.9
