# ETAPS 2017 Test of Time Award

The 2017 ETAPS Test of Time Award went to**Armin Biere, Alessandro Cimatti, Edmund M. Clarke and Yunshan Zhu**

for their TACAS 1999 paper

Symbolic model-checking without BDDs [doi link]

This paper made two fundamental and high-impact contributions to the field of model checking and automated verification.

The first involves the use ofÂ *general-purpose SAT solvers *to replace specialized decision procedures based on Boolean Decision Diagrams (BDDs) during the model-checking process. Before this paper, BDDs had been the cornerstone of so-called symbolic model checkers, which use implicit rather than explicit representations of the sets of system states they manipulate during their execution. BDDs had revolutionized model checking by enabling the handling of much larger systems than was previously possible. This paper was a revolutionary advance beyond BDDs, as the authors showed how the sets of states in question could also be viewed as propositional formulas that can be handled using general-purpose SAT solvers. This simple idea has had profound impact in the field of automated verification, as it is also the basis for the use of SMT solvers for model-checking of systems with, for example, infinite state spaces. Most modern model checkers now rely on a SAT-solving backend as a result of this paper.

The second fundamental contribution of the paper is the invention of the so-called *bounded model checking* technique for system verification. Before this paper, the goal of model checking was to prove systems correct; model checkers either found such a proof, or detected that no such proof was possible. This paper instead advocated the idea that the purpose of model checking was to detect bugs, and to give simplest-possible explanations for these bugs when they are uncovered. This change in perspective had a massive impact on model checking: it opened researchers up to the possibility of model-checking-inspired verification techniques that could give incremental information during the checking procedure, even if the procedure might not terminate in reasonable time with the classical "yes, there is a proof / no, no such proof exists" answer. Later "bug-search" techniques, such as statistical model checking and run-time verification, owe much of their inspiration to the bounded model-checking idea in this paper, even as this idea on its own continues to be a thriving area of research.

The 2017 Award Committee consisted of

Parosh Aziz Abdulla

Bruno Blanchet

Rance Cleaveland

Joost-Pieter Katoen

Luke Ong

Don Sannella (chair)

Zhong Shao

Gabriele Taentzer