Aaron Bradley

Date: 16:00, Thursday, June 27, 2013
Speaker: Aaron Bradley
Venue: IST Austria

16:00 – 17:00

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

Posted in RiSE Seminar