ETAPS 2018 Test of Time Award

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