LICS 2010 Test-of-time Award Winners

I just read an email announcing the papers selected for the 2010 LICS Test-of-Time Award. For the 2010 LICS Test-of-Time Award, all papers from LICS 1990 were considered by an Awards Committee consisting of Glynn Winskel (chair), Jean-Pierre Jouannaud and John Mitchell.

In view of the weight of highly-influential papers, across a range of areas, the committee has taken the exceptional step of selecting four papers! They are:

• Model-checking for real-time systems by R. Alur, C. Courcoubetis and D. Dill. This paper was a pioneer in the model checking of real-time systems. It provided a polynomial-space algorithm for the model checking of a real-time logic (an extension of CTL with timing constraints) with respect to a continuous-time model. Its techniques are still used extensively and results of this paper form part of almost any course or tutorial on real-time verification.
• Symbolic model checking: 10^20 states and beyond by JR Burch, EM Clarke, KL McMillan, DL Dill and LJ Hwang. This paper revolutionized model checking. Through its symbolic representation of the state space using Randy Bryant's Binary Decision Diagrams (BDDs) and its careful analysis of several forms of model checking problems, backed up by empirical results, it provided a first convincing attack on the verification of large-state systems. The paper was a major agent in establishing BDDs as a tool in mainstream computer science.
• The theory of ground rewrite systems is decidable by M Dauchet and S Tison. This paper asked what has proved to be a very important question, whether the first-order theory of one-step rewriting is decidable. The paper settled the question positively for the theory of ground rewrite systems using innovative techniques on tree automata. Its techniques rekindled an interest in automata theory on finite trees, now a major topic, with many current applications from rewriting through to security, program analysis and concurrency.
• Recursive types reduced to inductive types by P Freyd. This paper showed what was really going on with the classic method of solving domain equations.  By separating positive and negative occurrences of the unknown in a domain equation, it gave an elegant category-theoretic treatment of recursively defined domains that extends the well-understood and widely-used methods of initial-algebra semantics. Its methods are now standard. They led to new techniques for relating operational and denotational semantics, and new mixed induction/coinduction principles.

Congratulations to all the recipients of the awards!