The CAV award is given annually at the CAV conference for fundamental contributions to the field of Computer-Aided Verification. This years CAV Award winners are
| Clark Barrett | Stanford University |
| David Dill | Stanford University |
| Kyle Julian | Wing |
| Guy Katz | Hebrew University of Jerusalem |
| Mykel Kochenderfer | Stanford University |
for developing the Reluplex algorithm, which successfully applied computer-aided verificaon techniques to real-world deep neural networks.
Deep neural networks are a state-of-the-art machine learning technology, which has become dominant in many areas within computer science. In a groundbreaking CAV 2017 paper, titled “Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks”, the authors, Clark Barrett, David Dill, Kyle Julian, Guy Katz, and Mykel Kochenderfer, developed a novel SMT-based algorithm, Reluplex, for verifying deep neural networks. The original algorithm was written to help verify the “Airborne Collision-Avoidance System for drone” system (ACAS-Xu). Through Reluplex, the authors demonstrated, for the first time, that real-world neural networks could be verified. Reluplex could tackle neural networks that were over an order-of-magnitude larger as compared to previous verification techniques.
The Reluplex work had an immense impact on formal methods research, by creating a highly active sub-field within the verification community, which is now center-stage in every major verification conference and is also subject to an annual competition dedicated specifically to the verification of neural networks (VNN-COMP). The Reluplex algorithm has been extended and enhanced, by the authors and by others, and the original paper has already accumulated more than 2000 citations (as of May 2024) – making it one of the most well-cited CAV papers in the past decades. Following their initial work, the authors continue to play a key role in solidifying the field of neural network verification.
Please check here for the slides from Guy Katz’s CAV award talk.
NOMINATION
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.
For previous winners of the award, please see the main CAV award page. Nominations should be submitted by e-mail to a member of the committee.
IMPORTANT DATES
Nomination deadline: March 1, 2024
AWARD COMMITTEE
| Corina Pasareanu (Chair) | NASA |
| Rupak Majumdar | MPI-SWS |
| Ranjit Jhala | University of California, San Diego |
| Alessandro Cimatti | Fondazione Bruno Kessler |