MC@CU: Model Checking at CU Boulder

Research Overview

We develop new technologies for hardware (and sometimes software) verification. Our current focus is on developing a state-of-the-art parallel model checker, IImc, based on incremental, inductive verification (IIV), a perspective on model checking that has so far produced the IC3 algorithm for safety, the FAIR algorithm for LTL, and the IICTL algorithm for CTL.


Aaron Bradley (adjunct)

Fabio Somenzi
Old VLSI/CAD Research Group site

PhD Students

Michael Dooley Michael is a Ph.D. student focusing on word-level model checking.

Zyad Hassan Zyad received the B.Sc. degree in Electronics and Communications from Cairo University, Egypt, in 2006 and the M.Sc. degree in Electrical and Computer Engineering from the University of Colorado at Boulder in 2009. He is currently pursuing the Ph.D degree from the Department of Electrical and Computer Engineering at the University of Colorado at Boulder. His research interests include formal methods in computer-aided-design and model checking. He is currently working on algorithmic improvements to inductive model checkers.

Yan Zhang Yan is currently a Ph.D. student focusing on Formal Verification / Model Checking. Being trained as a digital/analog designer in his undergraduate, he easily got interested in the verification of sequential circuits. Now he is working in the MC@CU group on combinational/sequential optimization.


IImc: Under development, with version 1.0 about to be released. IImc provides research implementations of IC3 (for safety), FAIR (for LTL, more generally, ω-regular properties), and IICTL (for CTL &mdash in the next release), which are described in our papers and are based on our philosophy of incremental, inductive verification (IIV). IImc also applies BDD-based model checking and combinational and sequential optimizations. Placed first in the "UNSAT liveness" division in HWMCC'11.

IC3: The original parallel model checker based on inductive clause generation. The link contains binary and source downloads. Placed third in HWMCC'10. [Overview]

VIS: A model checking system.

CUDD: A BDD package.


Aaron R. Bradley, SAT-Based Model Checking Without Unrolling, VMCAI'11. Describes the fundamentally new technique of stepwise-relative inductive generalization, the basis of IC3 and IImc. [Slides] [Earlier presentation of work]

Aaron R. Bradley, Fabio Somenzi, Zyad Hassan, Yan Zhang, An Incremental Approach to Model Checking Progress Properties, FMCAD'11 (received "best paper" award). Describes how to apply the incremental, inductive technique pioneered in IC3 to ω-regular properties.

Fabio Somenzi and Aaron R. Bradley, IC3: Where Monolithic and Incremental Meet, Tutorial at FMCAD'11. Provides examples and historical/methodological context for IC3.

Zyad Hassan, Yan Zhang, Fabio Somenzi, "A Study of Sweeping Algorithms in the Context of Model Checking," DIFTS'11.

Zyad Hassan, Aaron R. Bradley, and Fabio Somenzi, Incremental, Inductive CTL Model Checking, CAV'12.

Aaron R. Bradley. Understanding IC3, SAT'12.

CU Boulder  |  ECEE