The papers are selected by an awards committee that is appointed by the LICS General Chair and consists of between three to five members. The committee is renewed every year; at the discretion of the General Chair, members may be reappointed to the awards committee.
In selecting these papers, the Awards Committee should consider the influence that the papers have had since publication; because of the foundational nature of LICS work, impact is often not fully felt immediately, hence the 20-year perspective.
The Award Committee is expected to select 1-2 papers. However, the Award Committee may choose to select no paper from a given year, or may select up to 3 papers.
All papers from the given year are eligible for this award, except those that are authored or co-authored by members of the Awards Committee. There is no formal nomination process for this award, but input from the LICS community is welcome.
List of all Test-of-Time Award winners
-
LICS Test-of-Time Award Winner in 2012
For the 2012 LICS Test-of-Time Award, all papers from LICS 1992 were considered. The Award Committee consisted of Martin Grohe, Prakash Panangaden, Andre Scedrov (Chair), and Ashish Tiwari. Two papers have been selected.
Thomas A. Henzinger Xavier Nicollin Joseph Sifakis Sergio Yovine
Symbolic model checking for real-time systemsMore Information...The paper made a crucial contribution to the success of symbolic model checking for analyzing timed and hybrid systems. The paper also led to the development of the Kronos tool, which was also very influential.
The paper was very influential in the programming language community. It paved the way for thinking of all kinds of new phenomena within the type-checking framework.
The presentation of the awards took place on June 27, 2012 during the Award Presentations session at LICS 2012.
-
LICS Test-of-Time Award Winner in 2011
For the 2011 LICS Test-of-Time Award, all papers from LICS 1991 were considered. The Award Committee consisted of Radha Jagadeesan, Tom Henzinger, Catuscia Palamidessi, and Andy Pitts (Chair). Three papers have been selected.
This is one of the papers behind "partial-order methods" in model checking, which is an important approach for fighting state explosion in the analysis of asynchronous systems. The paper established the theory for proving the correctness of partial-order algorithms for checking general temporal properties. This line of research was highly influential and affects the way explicit-state model checkers are being built today.
Joshua S. Hodas Dale A. Miller
Logic programming in a fragment of intuitionistic linear logicMore Information...This is one of the first explorations of logic programming style proof search in Girard's linear logic. The paper radically changed the perception of what logic programming might be, on the heels of linear logic changing the perception of what logic might be. In contrast to the traditional intuitionistic basis of logic programming, this new foundation permitted "stateful" (eg. modelling database updates) and "resourceful" (eg. in linguistic models) declarative models.
Dexter C. Kozen
A completeness theorem for Kleene algebras and the algebra of regular events More Information...This paper solved an important open problem to do with the axiomatization of the algebra of regular events. Although other solutions were found independently by Krob and Bloom-Esik, what made Kozen's solution in terms of conditional equations so influential is its elegant simplicity and generality. Kozen went on to develop from it a beautiful theory of Kleene algebras, with applications to various aspects of programming theory and logic.
The presentation of the awards took place on June 22, 2011 during the Award Presentations session at LICS 2011.
-
LICS Test-of-Time Award Winner in 2010
For the 2010 LICS Test-of-Time Award, all papers from LICS 1990 were considered. The Awards Committee consisted 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:
Rajeev Alur Costas Courcoubetis David L. Dill
Model-checking for real-time systemsMore Information...Brief Citation: 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.
Jerry R. Burch Edmund M. Clarke Kenneth L. McMillan David L. Dill L. James Hwang
Symbolic model checking: 10^20 states and beyondMore Information...Brief Citation: 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 verificationn of large-state systems. The paper was a major agent in establishing BDDs as a tool in mainstream computer science.
Brief Citation: 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.
Brief Citation: 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.
The presentation of the awards took place on July 12th, 2010 at the Business Meeting of LICS 2010.
-
LICS Test-of-Time Award Winner in 2009
For the 2009 LICS Test-of-Time Award, all papers from LICS 1989 were considered. The Awards Committee consisted of Rohit Parikh (chair), Phokion Kolaitis, and Glynn Winskel. The Committee has selected the following paper for the LICS Test-of-Time Award:
Brief Citation: Eugenio Moggi's LICS'89 paper changed the way we think about programs. According to the paper a program denotes a morphism from values to computations, and the nature of computations is determined by a monad. A 'computational lambda calculus' is built around this idea and shown to be sound and complete with respect to a categorical semantics. But more important than this technical result is the great unifying and systematizing power the ideas of the paper give to the semantics of computation. The paper has had a widespread influence on the theory of programming languages; monads are now a standard tool in modifying types.
The presentation of the award took place on August 12, 2009 during the Award Presentations session at LICS 2009.
-
LICS Test-of-Time Award Winner in 2008
For the 2008 LICS Test-of-Time Award, all papers from LICS 1988 were considered. The Awards Committee consisted of Rajeev Alur (Chair), Samson Abramsky, and Dexter Kozen. The Committee has selected the following paper for the LICS Test-of-Time Award:
Brief Citation: A central problem in formal approaches to system design and verification concerns establishing a refinement relationship between two descriptions of the system with different levels of detail. This paper shows that the method based on refinement maps is a complete proof technique provided the lower-level description is enriched with history and prophecy variables. The paper contains a conceptually clean solution to a practical verification problem, and the resulting ideas continue to provide guidance for designing specification languages as well as for formalizing correctness proofs of complex designs even today.
The presentation of the award took place on June 25, 2008 during the Award Presentations session at LICS 2008.
-
LICS Test-of-Time Award Winner in 2007
For the 2007 LICS Test-of-Time Award, all papers from LICS 1987 were considered. The Awards Committee consisted of Yuri Gurevich (Chair), Rajeev Alur, and Glynn Winskel. The Committee has selected the following two papers for the LICS Test-of-Time Award; the papers are listed in the order they appeared in the LICS 1987 proceedings:
The presentation of the awards took place on July 10, 2007 during the Awards Ceremony session at LICS 2007.
-
LICS Test-of-Time Award Winner in 2006
For the 2006 LICS Test-of-Time Award, all papers from LICS 1986 (the first LICS) were considered. The Awards Committee consisted of Samson Abramsky (Chair), Rajeev Alur, and Yuri Gurevich. The Committee has selected the following three papers for the LICS Test-of-Time Award; the papers are listed in the order they appeared in the LICS 1986 proceedings:
E. Allen Emerson Chin-Laung Lei
Efficient Model Checking in Fragments of the Propositional Mu-Calculus (Extended Abstract)More Information...Moshe Y. Vardi Pierre Wolper
An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report)More Information...The presentation of the awards took place on August 12, 2006 during the 2006 LICS Business Meeting.