Incremental, Inductive Model Checking

Author

Bradley, Aaron R.

Author_Institution

Univ. of Colorado at Boulder, Boulder, CO, USA

fYear

2013

fDate

26-28 Sept. 2013

Firstpage

5

Lastpage

6

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Temporal Representation and Reasoning (TIME), 2013 20th International Symposium on

Conference_Location

Pensacola, FL

ISSN

1530-1311

Print_ISBN

978-1-4799-2240-6

Type

conf

DOI

10.1109/TIME.2013.9

Filename

6786789