Prof. Aaron Stump and his co-authors* received one of two 2021 Test Of Time Awards, honoring papers published twenty years ago in the IEEE Symposium on Logic in Computer Science, which have "stood the test of time".  Prof. Stump's paper, "A Decision Procedure for an Extensional Theory of Arrays," was written while he was a doctoral student, and has been influential in the field of Satisfiability Modulo Theories (SMT).

"This is the first paper on a dedicated decision procedure for the theory of arrays, one of the most important theories in applications of Satisfiability Modulo Theories (SMT), particularly in combination with bit-vectors for bit-precise reasoning. These applications include symbolic-execution (e.g., SAGE) and bounded-model checking of software and hardware (CBMC). Thus it was highly influential and formed the basis for other high impact papers in SMT." 

* Clark W. Barrett (Stanford);  David L. Dill (Stanford Emeritus Faculty; Lead Researcher, Blockchain at Facebook); Jeremy R. Levitt (Principal Engineer at Siemens EDA)