Aaron Bradley's Home Page

Aaron R. Bradley

Math teacher at Summit Charter Middle School in Boulder, CO. Go Huskies!
Adjunct (research) professor in ECEE at CU Boulder. MC@CU

The Calculus of Computation: Decision Procedures with Applications to Verification.
- Published by Springer-Verlag, 2007.
- A graduate-level text co-authored with Zohar Manna.
- Accompanying software: πVC, the Pi Verifying Compiler.
Programming for Engineers.
- Published by Springer-Verlag, 2011.
- A first-year course for engineers on programming.
- Source code from the text.

Incremental, inductive verification (i.e., the IC3 model checker and more)
- Safety properties:
  - Aaron R. Bradley, SAT-Based Model Checking without Unrolling, VMCAI 2011. [PDF] [Slides] [Software]
  - Aaron R. Bradley, Understanding IC3, SAT 2012. [PDF] [SSFT'12 Slides] [SAT'12 Slides] [CAV'12 Slides]
  - What's Happening with IC3? [HVC'12 Slides]
  - Fabio Somenzi and Aaron R. Bradley, IC3: Where Monolithic and Incremental Meet, FMCAD 2011. [PDF] (Tutorial on IC3 given by Fabio)
  - Technical report from March, 2010, on arXiv.
  - Aaron R. Bradley and Zohar Manna, Checking Safety by Inductive Generalization of Counterexamples to Induction, FMCAD 2007. [PS] [PDF] [Slides]
- ω-regular properties:
  - Aaron R. Bradley, Fabio Somenzi, Zyad Hassan, Yan Zhang, An Incremental Approach to Model Checking Progress Properties, FMCAD 2011. [PDF]
- CTL properties:
  - Zyad Hassan, Aaron R. Bradley, and Fabio Somenzi, Incremental, Inductive CTL Model Checking, CAV 2012. [PDF]
Aaron R. Bradley, Zohar Manna, Henny B. Sipma, What's Decidable About Arrays?, VMCAI 2006. [PS] [PDF] [Slides]
Thesis: Safety Analysis of Systems, May 2007. [PDF]
List with older stuff, though anything worth reading is above.