CAV Award | International Conference on Computer-Aided Verification (original) (raw)
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.
| Year | Recipient(s) | Citation |
|---|---|---|
| 2008 | Rajeev Alur, University of PennsylvaniaDavid L. Dill, Stanford University. | For fundamental contributions to the theory of real-time systems verification. |
| 2009 | Conor F. Madigan, Kateeva, Inc.Sharad Malik, Princeton UniversityJoão P. Marques-Silva, University College Dublin, IrelandMatthew W. Moskewicz, University of California, BerkeleyKarem A. Sakallah, University of MichiganLintao Zhang, Microsoft ResearchYing 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 ResearchSriram 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, SRIJohn Rushby, SRINatarajan 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 AalborgPaul Pettersson, Mälardalen UniversityWang 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 ResearchDoron Peled, Bar Ilan UniversityAntti Valmari, Tampere University of TechnologyPierre 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 LondonJohn Reynolds, Carnegie Mellon Hongseok Yang University of Oxford | For the development of Separation Logic and for demonstrating itsapplicability in the automated verification of programs that mutatedata structures. |
| 2017 | Parosh 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. |
| 2018 | Armin 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). |
| 2019 | Jean-Christophe FilliâtreK. 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. |
| 2020 | Due to the ongoing COVID-19 pandemic no award was selected. | |
| 2021 | Gilles Audemard, Université d’Artois, FranceClark Barrett, Stanford UniversityPiergiorgio Bertoli, Fondazione Bruno Kessler, Trento, ItalyNikolaj Bjørner, Microsoft ResearchRandal E. Bryant, Carnegie Mellon UniversityAlessandro Cimatti, Fondazione Bruno Kessler, Trento, ItalyDavid Dill, Stanford UniversityBruno Dutertre, SRI InternationalHarald Ganzinger, (1950 – 2004)George Hagen, NASA Langley Research CenterArtur Korniłowicz, University of Bialystok Shuvendu Lahiri, Microsoft ResearchLeonardo de Moura, Microsoft ResearchRobert Nieuwenhuis, Technical University of CataloniaAlbert Oliveras, Technical University of CataloniaHarald Rueß, fortissRoberto Sebastiani, Università di Trento Sanjit A. Seshia, University of California, BerkeleyOfer Strichman, TechnionAaron 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). |
| 2022 | Susanne Graf, Hassan Saidi | For their pioneering work on predicate abstraction. |
| 2023 | Jakob Rehof, TU DortmundThomas Reps, UW-MadisonAkash Lal, Microsoft ResearchShaz Qadeer, Meta ResearchMadan Musuvathi, Microsoft Research | For the introduction of context-bounded analysis and its application to the systematic testing of concurrent programs. |
| 2024 | Clark Barrett, Stanford UniversityDavid Dill, Stanford UniversityKyle Julian, WingGuy Katz, Hebrew University of JerusalemMykel Kochenderfer, Stanford University | For developing the Reluplex algorithm, which successfully applied computer-aided verification techniques to real-world deep neural networks. |