Aaron Bradley
New website.
I earned my Ph.D. under the advisorship of Zohar Manna in the department of Computer Science at Stanford University. Through December, I am visiting Tom Henzinger's group at EPFL. Starting in January 2008, I will be an assistant professor in the department of Electrical & Computer Engineering at CU Boulder.
You may reach me here, unless I'm in the sky or hiking/cycling in the mountains.
My wife, Sarah, is a software developer at Quia.
My brother, Andrew, is a Ph.D. student in the ICME department. Here, we're sharing the air; and here we are after four days on the road.
Implementation of Cooper's quantifier-elimination method for Presburger arithmetic (last updated 12/02/2007). The main code, for those who want a quick look. See Chapter 7 of COC for an explanation.
Aaron R. Bradley and Zohar Manna, Property-Directed Incremental Invariant Generation, To appear in Formal Aspects of Computing, 2008. [PS] [PDF]
Aaron R. Bradley and Zohar Manna, Checking Safety by Inductive Generalization of Counterexamples to Induction, In Proc. Formal Methods in Computer Aided Design (FMCAD) November 2007. [PS] [PDF] [Slides]
Thesis: Safety Analysis of Systems, May 2007. [PDF] Recent slides on Ch. 2: [PDF]
Aaron R. Bradley and Zohar Manna, Verification Constraint Problems with Strengthening, In Proc. International Colloquium on Theoretical Aspects of Computing (ICTAC) November 2006, Lecture Notes in Computer Science, Volume 4281, Springer-Verlag. Invited Paper. [PS] [PDF]
Aaron R. Bradley, Zohar Manna, Henny B. Sipma, What's Decidable About Arrays?, In Proc. Verification, Model-Checking, and Abstract-Interpretation (VMCAI) January 2006, Lecture Notes in Computer Science, Volume 3855, Springer-Verlag. [PS] [PDF] [Slides]
Aaron R. Bradley, Zohar Manna, Henny B. Sipma, Termination Analysis of Integer Linear Loops, In Proc. Concurrency Theory (CONCUR) August 2005, Lecture Notes in Computer Science, Volume 3653, Springer-Verlag. [PS] [PDF] [Slides]
Aaron R. Bradley, Zohar Manna, Henny B. Sipma, The Polyranking Principle, In Proc. International Colloquium on Automata, Languages and Programming (ICALP) July 2005, Lecture Notes in Computer Science, Volume 3580, Springer-Verlag. [PS] [PDF] [Slides]
Aaron R. Bradley, Zohar Manna, Henny B. Sipma, Linear Ranking with Reachability, In Proc. Computer Aided Verification (CAV) July 2005, Lecture Notes in Computer Science, Volume 3576, Springer-Verlag. [PS] [PDF] [Slides]
Aaron R. Bradley, Zohar Manna, Henny B. Sipma,
Termination of Polynomial Programs,
In Proc. Verification, Model-Checking, and Abstract-Interpretation
(VMCAI) January 2005,
Lecture Notes in Computer Science, Volume 3385, Springer-Verlag.
[PS]
[PDF]
[Slides]
Extended version:
Polyranking for Polynomial Loops.
[PS]
[PDF]
After 20+ years of dreaming, I've finally grown wings. Well, sort of. It's called paragliding, and it's about the closest thing to soaring like an eagle (hawk, turkey vulture, etc.) there is. The wing is a Gin Yeti. I'm soaring at the Dumps in Pacifica (Mussel Rock). Photos courtesy of Doug Wolf. Check out Andrew's account of our flying adventures.
I'm playing around with Photoshop and a tablet-input device. Experiments that did not go terribly wrong: What's so funny?, ACM 25th Chimposium on Computer Science (thanks to Sriram for the idea), Stop!, In the Beginning, Cruisin', Monitor Bears, Ergo, Constitutional, The Shaggies
Celebrating the discovery of the molecule of life (H2O, for those of you unaware of Homo snowpien biology). You want it bigger? Fine. For more geek cartoons, see The Door of Gates 488.
Did somebody say lizard? Aren't they cute? No? Maybe you prefer mammals. Try this.
Poster for the annual Bike to School Week at Hoover Elementary School. The space in the lower-right region is for the year.
My undergraduate honors thesis (2002). [PS] [PDF]
