CAV Award

The CAV award is given annually at the CAV conference for fundamental contributions to the field of Computer-Aided Verification. The award comes with a cash prize of US$10,000 shared equally among recipients.

Anyone can submit a nomination for the CAV award. For information on nominations, please see the web site of the upcoming conference.

 CAV Award Recipients

Year Recipent(s) Citation
2008 Rajeev Alur, University of Pennsylvania
David L. Dill, Stanford University.
For fundamental contributions to the theory of real-time systems verification.
2009 Conor F. Madigan, Kateeva, Inc.
Sharad Malik, Princeton University
João P. Marques-Silva, University College Dublin, Ireland
Matthew W. Moskewicz, University of California, Berkeley
Karem A. Sakallah, University of Michigan
Lintao Zhang, Microsoft Research
Ying Zhao, Wuxi Capital Group
For major advances in creating high-performance Boolean satisfiability solvers.
2010 Kenneth L. McMillan, Cadence Research Laboratories. For a series of fundamental contributions resulting in significant advances in scalability of model checking tools.
2011 Thomas Ball, Microsoft Research
Sriram Rajamani, Microsoft Research
For their contributions to software modelchecking, specifically the development of the SLAM/SDV software model checker, which successfully demonstrated computer-aided verification techniques on real programs.
2012 Sam Owre, SRI
John Rushby, SRI
Natarajan Shankar, SRI
For developing PVS (Prototype Verification System) which, due to its early emphasis on integrated decision procedures and user friendliness, significantly accelerated the application of proof assistants to real-world verification problems.
2013 Kim G. Larsen, University of Aalborg
Paul Pettersson, Mälardalen University
Wang Yi, Uppsala University
For developing UPPAAL which is the foremost tool suite for the automated analysis and verification of real-time systems.
2014 Patrice Godefroid, Microsoft Research
Doron Peled, Bar Ilan University
Antti Valmari, Tampere University of Technology
Pierre Wolper, Université de Liege
For the development of partial-order reduction algorithms for efficient state-space exploration of concurrent systems.
2015 Edmund M. Clarke, Carnegie-Mellon
Orna Grumberg, Technion
Ronald H. Hardin 
Somesh Jha, University of Wisconsin 
Yuan Lu
Robert P. Kurshan 
Helmut Veith, FORSYTE 
Zvi Harel
For the development and implementation of the localization-reduction technique and the formulation of counterexample-guided abstraction refinement.
2016 Josh Berdine, Facebook
Cristiano Calcagno, Facebook
Dino Distefano, Facebook and Queen Mary University of London
Samin Ishtiaq, Microsoft Research Cambridge
Peter O’Hearn, Facebook and University College London
John Reynolds, Carnegie Mellon
Hongseok Yang University of Oxford
For the development of Separation Logic and for demonstrating its
applicability in the automated verification of programs that mutate
data structures.