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]
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]