The 2021 CAV Award recognizes the “pioneering contributions to the foundations of the theory and practice of satisfiability modulo theories (SMT).”
In 2002, in the wake of the “Satisfiability Revolution,” in which the performance of solvers for propositional satisfiability (SAT) improved dramatically, a number of research groups in automated reasoning and formal methods independently developed the idea of leveraging these new fast SAT solvers to reason about more expressive theories in first-order logic. This breakthrough idea of using a SAT solver as the main driver of search was the critical seed that launched the research area now known as Satisfiability Modulo Theories (SMT). The development and use of SMT solvers has grown dramatically since then, and SMT solvers are now critical enablers for a wide variety of efforts in verification and many adjacent fields. Applications using SMT solvers in verification include: software and hardware model checking, symbolic execution, program verification, compiler verification, verifying cyber- physical systems, and program synthesis. Applications beyond verification include: planning, biological modeling, database integrity, network security, scheduling, and automatic exploit generation. In this nomination, we propose to recognize contributors whose pioneering works laid the groundwork for the theory and practice of SMT.
Pierre Wolper
Somesh Jha
Parosh Abdulla
Corina Pasareanu
The 2021 CAV Award Committee
The recipients are:
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
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.
For previous winners of the award, please see the main CAV award page.
Award Committee
Pierre Wolper, Liege University (chair)
Somesh Jha, University of Wisconsin
Parosh Abdulla, Uppsala University
Corina Pasareanu, NASA