| 2014 | CAV | Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR). | Johannes Birgmeier, Aaron R. Bradley, Georg Weissenbacher |
| 2013 | FMCAD | Better generalization in IC3. | Zyad Hassan, Aaron R. Bradley, Fabio Somenzi |
| 2013 | TIME | Incremental, Inductive Model Checking. | Aaron R. Bradley |
| 2012 | CAV | IC3 and beyond: Incremental, Inductive Verification. | Aaron R. Bradley |
| 2012 | CAV | Incremental, Inductive CTL Model Checking. | Zyad Hassan, Aaron R. Bradley, Fabio Somenzi |
| 2012 | SAT | Understanding IC3. | Aaron R. Bradley |
| 2011 | FMCAD | An incremental approach to model checking progress properties. | Aaron R. Bradley, Fabio Somenzi, Zyad Hassan, Yan Zhang |
| 2011 | FMCAD | IC3: where monolithic and incremental meet. | Fabio Somenzi, Aaron R. Bradley |
| 2011 | VMCAI | SAT-Based Model Checking without Unrolling. | Aaron R. Bradley |
| 2007 | FMCAD | Checking Safety by Inductive Generalization of Counterexamples to Induction. | Aaron R. Bradley, Zohar Manna |
| 2006 | ICTAC | Verification Constraint Problems with Strengthening. | Aaron R. Bradley, Zohar Manna |
| 2006 | VMCAI | What's Decidable About Arrays? | Aaron R. Bradley, Zohar Manna, Henny B. Sipma |
| 2005 | ATVA | Termination and Invariance Analysis of Loops. | Aaron R. Bradley, Zohar Manna |
| 2005 | CAV | Linear Ranking with Reachability. | Aaron R. Bradley, Zohar Manna, Henny B. Sipma |
| 2005 | CONCUR | Termination Analysis of Integer Linear Loops. | Aaron R. Bradley, Zohar Manna, Henny B. Sipma |
| 2005 | ICALP | The Polyranking Principle. | Aaron R. Bradley, Zohar Manna, Henny B. Sipma |
| 2005 | VMCAI | Termination of Polynomial Programs. | Aaron R. Bradley, Zohar Manna, Henny B. Sipma |