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. The Award Committee can originate a nomination. Anyone, with the exception of members of the Award Committee, is eligible to receive the Award. A nomination must state clearly the contribution(s), explain why the contribution is fundamental or the series of contributions is outstanding, and be accompanied by supporting letters and other evidence of worthiness.

Nominations should include a proposed citation (up to 25 words), a succinct (100-250 words) description of the contribution(s), and a detailed statement to justify the nomination. The cited contribution(s) must have been made not more recently than five years ago and not over twenty five years ago. In addition, the contribution(s) should not yet have received recognition via a major award, such as the ACM Turing or Kanellakis Awards. The nominee may have received such an award for other contributions. 

Nominations should be submitted by e-mail to a member of the committee. For nomination deadlines and listing of the current committee, please see the the web site of the upcoming conference, linked in the menu above.

 CAV Award Recipients

2008Rajeev Alur, University of Pennsylvania
David L. Dill, Stanford University.
For fundamental contributions to the theory of real-time systems verification.
2009Conor 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.
2010Kenneth L. McMillan, Cadence Research Laboratories.For a series of fundamental contributions resulting in significant advances in scalability of model checking tools.
2011Thomas 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.
2012Sam 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.
2013Kim 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.
2014Patrice 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.
2015Edmund 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.
2016Josh 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.
2017Parosh Abdulla,
Alain Finkel,
Bengt Johnsson,
Philippe Schnoebelen
For the development of general mathematical structures leading to general decidability results for the verification of infinite-state transition systems.
2018Armin Biere,
Alessandro Cimatti,
Edmund M. Clarke,
Daniel Kroening,
Flavio Lerda,
Yunshan Zhu
For their outstanding contribution to the enhancement and scalability of model checking by introducing Bounded Model Checking based on Boolean Satisfiability (SAT) for hardware (BMC) and software (CBMC).
2019Jean-Christophe Filliâtre
K. Rustan M. Leino
For the design and development of reusable intermediate verification languages that have significantly simplified and accelerated the construction of practical automated deductive verifiers.

Due to the ongoing COVID-19 pandemic no award was selected.


Gilles Audemard, Université d’Artois, France
Clark Barrett, Stanford University
Piergiorgio Bertoli, Fondazione Bruno Kessler, Trento, Italy
Nikolaj Bjørner, Microsoft Research
Randal E. Bryant, Carnegie Mellon University
Alessandro Cimatti, Fondazione Bruno Kessler, Trento, Italy
David Dill, Stanford University
Bruno Dutertre, SRI International
Harald Ganzinger, (1950 – 2004)
George Hagen, NASA Langley Research Center
Artur Korniłowicz, University of Bialystok
Shuvendu Lahiri, Microsoft Research
Leonardo de Moura, Microsoft Research
Robert Nieuwenhuis, Technical University of Catalonia
Albert Oliveras, Technical University of Catalonia
Harald Rueß, fortiss
Roberto Sebastiani, Università di Trento
Sanjit A. Seshia, University of California, Berkeley
Ofer Strichman, Technion
Aaron Stump, University of Iowa
Cesare Tinelli, University of Iowa

For pioneering contributions to the foundations of the theory and practice of satisfiability modulo theories (SMT).


Susanne Graf, Hassan Saidi

For their pioneering work on predicate abstraction.

2023Jakob Rehof, TU Dortmund
Thomas Reps, UW-Madison
Akash Lal, Microsoft Research
Shaz Qadeer, Meta Research
Madan Musuvathi, Microsoft Research
For the introduction of context-bounded analysis and its application to the systematic testing of concurrent programs