HVC Award

Granted since 2007, the HVC award recognizes the most promising academic and industrial contribution to the fields of testing and software and hardware verification from the last five years.

Prof. Aaron R. BradleyThe HVC 2012 Award Committee, chaired by Prof. Daniel Kroening, has decided to give this year's award to Prof. Aaron R. Bradley of CU Boulder for the invention of the IC3 algorithm.

IC3 is an algorithm for verifying reachability properties on finite-state transition systems, and has been proposed by Aaron Bradley, CU Boulder. There are independent reports of leading performance on hardware-verification problems, which is impressive given the decades of research on competing techniques, including BDDs and recent innovations such as Craig interpolation with propositional SAT. The technique has been picked up by others, as evidenced by a variant of the algorithm for software presented at CAV this year. The committee believes that IC3 has innovated this mature research area, and produced new impulses for numerous adjacent research problems.

The HVC2012 Award Committee:

Daniel Kroening (Chair)
Marta Kwiatkowska
Roderick Bloem
John W O'Leary
Rupak Majumdar

Award talk abstract

IC3 is a model checking algorithm for invariant properties inspired by the deductive methodology. It 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 refinements to approximate i-step state sets in response to concrete error states. In this talk, I will provide an overview of IC3, two algorithms for LTL and CTL model checking that it inspired, and my research group's ongoing work on IC3-like approaches to analyzing infinite-state systems.