The 2021 ETAPS Test of Time Award went to

Sarfraz Khurshid, Corina S. Păsăreanu and Willem Visser

for their TACAS 2003 paper

Generalized Symbolic Execution for Model Checking and Testing [doi].

This paper is noteworthy for its combined use of symbolic execution and model checking to both verify software applications and to generate exhaustive test cases for them. At the time of the work’s publication, the predominant approaches to conducting these validation tasks on actual software involved applying user-defined abstractions to the source code in question to derive models that could then be fed into existing model-checking / test-generation tools. This paper showed that by using symbolic execution, the abstraction step could be omitted, and that constraint solvers could be used in conjunction with symbolic execution to undertake both full verification as well as the task of automated test generation. The resulting technology has been implemented in the widely used Java PathFinder tool and is still a key piece of that technology’s functionality, almost 20 years later. In addition, the combination of symbolic execution and model checking is used nowadays in many different applications such as the verification of implementations of communication protocols.

The 2021 award committee consisted of

Rance Cleaveland
Ugo Dal Lago
Marieke Huisman
Peter Y. A. Ryan
Don Sannella (chair)
Gabriele Taentzer
Peter Thiemann