Test of Time Award

The ETAPS Test of Time Award, instituted 2017, recognizes outstanding papers published more than 10 years in the past in one of the constituent conferences of ETAPS. The Award recognises the impact of excellent research results that have been published at ETAPS.

The Test of Time Award is selected by an Award Committee consisting of a representative of each of the constituent ETAPS conferences, the ETAPS Steering Committee Chair, the General Chair of the current ETAPS, and a Chair appointed by the ETAPS Steering Committee Chair. The Award Committee is expected to select 1-2 papers each year. It may choose to select no paper in a given year.

The winners of the ETAPS Test of Time Award receive a recognition plaque at ETAPS and a cash award of 1000€ which is shared among the authors. A paper can receive the ETAPS Test of Time Award only once.

2018

The 2018 ETAPS Test of Time Award went to

• Leonardo de Moura and Nikolaj Bjørner

for their TACAS 2008 paper

• Z3: An Efficient SMT Solver [doi link].

This paper introduces the Z3 “satisfaction modulo theories” (SMT) solver and describes some of its uses within Microsoft Research at the time of the paper’s writing. The so-called SMT problem solved by Z3 is easy to state: given a list of quantifier-free first-order formulas, determine if there exists an assignment of values to free variables in the formulas that makes all the formulas true. Z3 combines SAT-solving with constraint solvers for specific theories to accomplish this task. The tool is structured in an elegant way, making it relatively easy to extend the theories that the tool supports. It is also well-engineered, making it very efficient, and supporting materials that have been developed over the years make it straightforward to learn and use.

For these reasons, Z3 has become the standard SMT used in program-analysis and system verification engines, from static analyzers for programming languages, to test-case generators for modeling languages such as Simulink, to model checkers for various system-modeling tools in which data features prominently. The tool is now available under an open-source license. It has bindings for a number of programming languages, including C, C++, Java, OCaml and Python, and has become the default SMT solver used in research projects worldwide.

Despite the short length (4 pages!) of this paper, it is the standard reference for the Z3 tool. It is also almost certainly the most heavily cited ETAPS paper to date, at least according to Google Scholar.

The 2018 Award Committee consisted of

• Bruno Blanchet,
• Rance Cleaveland,
• Joost-Pieter Katoen,
• Panagiotis Katsaros,
• Luke Ong,
• Don Sannella (chair),
• Gabriele Taentzer,
• Hongseok Yang.

2017

The 2017 ETAPS Test of Time Award was won by

• 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.