Aaron R. Bradley

Research

• IC3 for safety properties:
  • Aaron R. Bradley, SAT-Based Model Checking without Unrolling, VMCAI 2011. [PDF]
  • Zyad Hassan, Aaron R. Bradley, Fabio Somenzi, Better Generalization in IC3, FMCAD 2013. [PDF]
  • Aaron R. Bradley and Zohar Manna, Checking Safety by Inductive Generalization of Counterexamples to Induction, FMCAD 2007. [PDF]
• Extensions:
  • Aaron R. Bradley, Fabio Somenzi, Zyad Hassan, Yan Zhang, An Incremental Approach to Model Checking Progress Properties, FMCAD 2011. [PDF]
  • Zyad Hassan, Aaron R. Bradley, and Fabio Somenzi, Incremental, Inductive CTL Model Checking, CAV 2012. [PDF]
  • Johannes Birgmeier, Aaron R. Bradley, and Georg Weissenbacher, Counterexample to Induction-Guided Abstraction-Refinement (CTIGAR), CAV 2014. [PDF]
• Older papers

Books

• 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.