Aaron R. Bradley
- Incremental, inductive verification (i.e., the IC3 model checker and more)
- Safety properties:
- Implementing an IC3-related project? Consider using this reference implementation, which is relatively small, competitive, and well commented.
- "The" IC3 paper: Aaron R. Bradley, SAT-Based Model Checking without Unrolling, VMCAI 2011.
[New Reference Implementation]
- For the curious, a technical report from March 2010 that fully describes IC3: arXiv.
- Where inductive clause extraction was first described:
Aaron R. Bradley and Zohar Manna,
Checking Safety by Inductive Generalization of Counterexamples to
Induction, FMCAD 2007.
- An improvement to generalization: Zyad Hassan, Aaron R. Bradley, Fabio Somenzi, Better Generalization in IC3, FMCAD 2013. [PDF]
- Aaron R. Bradley, Fabio Somenzi, Zyad Hassan, Yan Zhang,
An Incremental Approach to Model Checking Progress Properties, FMCAD 2011.
- Zyad Hassan, Aaron R. Bradley, and Fabio Somenzi, Incremental,
Inductive CTL Model Checking, CAV 2012.
With abstraction-refinement (for SMT-/word-level analysis):
- Johannes Birgmeier, Aaron R. Bradley, and Georg Weissenbacher, Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR), CAV 2014. [PDF]
Aaron R. Bradley, Zohar Manna, Henny B. Sipma,
What's Decidable About Arrays?, VMCAI 2006.
- Thesis: Safety Analysis of Systems, May 2007. [PDF]
- List with older stuff, though anything worth reading is above.
Web-worthy (which ain't sayin' much) Interests
- Some drawings. Whiteboard doodles.
- Some bicycle tour logs:
- Prince Edward Island (with Sarah, pics only) (July 2011, 12 days)
- Boulder-Yellowstone Loop (July 2010, 11 days)
- Boulder, CO to Skokie, IL (June 2009, 11 days)
- RMNP (October 2008, 2 days)
- Mt. Evans (with Sarah, pics only) (August 2008, 6 days)
- Mt. Evans (solo) (July 2008, 2 days)
- Tandem loop through parts of CO, NE, WY (May 2008, 13 days)