The CAV award is given annually at the CAV conference for fundamental contributions to the field of Computer-Aided Verification.
The CAV Award 2025 goes to Roy Armoni, Ilan Beer, Shoham Ben-David, Cindy Eisner, Dana Fisman, Limor Fix, John Havlicek, Avner Landver, Hiller Miller, and Moshe Vardi “for fundamental contributions in designing temporal logics that led to highly successful industry-standard property-specification languages based on temporal logics such as ForSpec, Sugar, PSL, and SVA.”
Please see here for the slides of the talk.
Temporal logics and automata are robust and expressive languages for formal descriptions of system requirements. They enable the use of automated or interactive verification of system properties. While the theoretical foundations of temporal logics and automata, together with model-checking algorithms, were worked out by the 1990s, the journey from these foundations to industrial practice required further breakthroughs.
The IBM and Intel teams developed two industrial property specification languages: ForSpec (Intel) and Sugar (IBM), built on a body of prior theoretical work on temporal and dynamic logics as well as tools (Forecast and RuleBase) that implement these languages. Language design was also inspired with earlier experience at both IBM and Intel with industrial model checking. Both IBM and Intel sent representatives to Accellera, where they worked together to “merge” ForSpec and Sugar into PSL. The language combines temporal connectives from Linear Temporal Logic with dynamic operators borrowed from Propositional Dynamic Logic as well as syntactic sugar for common industrial patterns. PSL has become an industry standard, led to SVA, another industry standard, and has contributed significantly to the adoption of model-checking technology in the semiconductor industry.
The CAV Award recognizes the efforts of the industrial teams in continuing the journey from academic foundations to industrial adoption. Formal methods and model checking have become part of the design process in the hardware industry and this early work inspired many new innovations—both in expressiveness and in scalability of analysis—in subsequent years.
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 this year’s chair, Rupak Majumdar.
IMPORTANT DATES
Nomination Deadline: March 4, 2025
AWARD COMMITTEE
Rupak Majumdar, MPI-SWS (Chair)
Ranjit Jhala, University of California, San Diego
Alessandro Cimatti, Fondazione Bruno Kessler
Işıl Dillig, University of Texas, Austin