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. With this prize, we recognize contributors whose pioneering works laid the groundwork for the theory and practice of SMT.