Prof. Sarfraz Khurshid of Texas ECE has been named a recipient of the 2021 European Joint Conferences on Theory and Practice of Software (ETAPS) Test of Time Award for his paper on "Generalized Symbolic Execution for Model Checking and Testing." The paper was co-authored by Corina S. Păsăreanu and Willem Visser and published in 2003.
According to ETAPS, 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 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 recognizes 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.
Dr. Sarfraz Khurshid is a Professor of Electrical and Computer Engineering at The University of Texas at Austin.
He completed his PhD in Computer Science at MIT. He received a BSc in Mathematics and Computer Science from Imperial College (London), and read Part III of the Mathematical Tripos at Trinity College Cambridge. He is the recipient of the ACM SIGSOFT Impact Paper Award (2012), two ACM SIGSOFT Distinguished Paper Awards (ISSTA 2002 and ICSE 2010), a Best Practical Paper Award (IEEE S&P Oakland 2014), a Best Research Paper Award (ASWEC 2009), and an NSF CAREER Award (2009).
