Computer Aided Verification
In computer science, the International Conference on Computer-Aided Verification (CAV) is an annual academic conference on the theory and practice of computer-aided formal analysis of software and hardware systems, broadly known as formal methods. Among the important results originally published in CAV are techniques in model checking, such as Counterexample-Guided Abstraction Refinement[1] and partial order reduction.[2][3] It is often ranked among the top conferences in computer science.[4][5]
The first CAV was held in 1989 in Grenoble, France. The CAV proceedings (1989-present) are published by Springer Science+Business Media. They have been open access since 2018.[6][7][8]
CAV Award
The annual CAV award was started in 2008.[9]
| Year | Recipients | 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 Somesh Jha, University of Wisconsin Yuan Lu Helmut Veith, FORSYTE |
"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." |
| 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,
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âtre | "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, 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)." |
| 2022 | Susanne Graf, Hassan Saidi | "For their pioneering work on predicate abstraction." |
| 2023 | Jakob 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." |
| 2024 | 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 verification techniques to real-world deep neural networks." |
See also
- List of computer science conferences
- Symposium on Logic in Computer Science
- European Joint Conferences on Theory and Practice of Software
References
- ^ Clarke, Edmund M.; et al. (2000). "Counterexample-Guided Abstraction Refinement". Computer Aided Verification. Lecture Notes in Computer Science. Vol. 1855. pp. 154–169. doi:10.1007/10722167_15. ISBN 978-3-540-67770-3.
- ^ Valmari, Antti (1990). "A Stubborn Attack On State Explosion". Computer-Aided Verification. Lecture Notes in Computer Science. Vol. 531. pp. 156–165. doi:10.1007/BFb0023729. ISBN 978-3-540-54477-7.
- ^ Godefroid, Patrice (1990). "Using Partial Orders to Improve Automatic Verification Methods". Computer-Aided Verification. Lecture Notes in Computer Science. Vol. 531. pp. 176–185. doi:10.1007/BFb0023731. ISBN 978-3-540-54477-7.
- ^ "Ranked Conference List (2010)". Australian Research Council. Archived from the original on 27 February 2012. Retrieved 3 January 2012.
- ^ "Top conferences in Software Engineering". Microsoft Academic Search. Archived from the original on 29 June 2013. Retrieved 3 January 2012.
- ^ Chockler, Hana; Weissenbacher, Georg, eds. (2018). "Computer Aided Verification". Lecture Notes in Computer Science. doi:10.1007/978-3-319-96142-2. ISSN 0302-9743.
- ^ Majumdar, Rupak; Kunčak, Viktor, eds. (2017). "Computer Aided Verification". Lecture Notes in Computer Science. doi:10.1007/978-3-319-63390-9. ISSN 0302-9743.
- ^ Enea, Constantin; Lal, Akash, eds. (2023). "Computer Aided Verification". Lecture Notes in Computer Science. doi:10.1007/978-3-031-37703-7. ISSN 0302-9743.
- ^ a b "CAV Award". i-cav.org/cav-award/. Retrieved October 25, 2024.
External links
| International | |
|---|---|
| National | |
 | This computer science article is a stub. You can help Wikipedia by expanding it. |