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 2024
All papers from LICS 2004 were considered for the 2024 LICS Test-of-Time Award. The Award Committee consisted of Franz Baader (chair), Karoliina Lehtinen, Prakash Panangaden, and Albert Rubio.
This extraordinary paper has had a major impact on the development of quantum computation in the logic and computation community. It has led to new algebraic and diagrammatic ways of thinking about quantum computation and has stimulated research on quantum programming languages, calculi for reasoning about quantum computation, and lately even error correction. Using the logic of compact closed categories, the paper gives an abstract treatment of fundamental aspects of quantum mechanics and quantum computation, with only sparse use of the usual mathematical machinery (such as linear algebra and Hilbert spaces). It shows that major protocols of quantum computation, such as teleportation and entanglement swapping, can not only be formulated, but also proved to be correct in this framework. Fundamental aspects of quantum mechanics are given an abstract treatment, most notably the Born rule. In summary, this paper began and gave impetus to the development of an abstract way to reason about quantum mechanics and quantum computation. It is very highly cited and has had major impact on reasoning about quantum computation and quantum mechanics.
The paper presents in a very clean and elegant way a general characterization of the validity of liveness properties of programs, like ter- mination and other such properties expressed in temporal logic. This is achieved by employing relations over program states, called transition in- variants, which contain the transitive closure of the state transition relation defined by the program. The key result is that the absence of infinite ex- ecutions can be reduced to proving that the transition invariant is a finite union of well-founded relations. The authors show how to use such dis- junctively well-founded transition invariants to validate temporal properties of concurrent systems. The paper has greatly influenced the development of techniques and tools for proving termination of programs automatically since it nicely combines the use of disjunctive well-foundedness with the construction of an abstraction of the program transition relation, which is the transition invariant. The suitability for automation of the approach has been crucial in its success. In addition, the paper also had a large impact on the design of powerful techniques based on termination analysis to (dis)prove a great variety of temporal properties of programs.
The presentation of the award took place at LICS 2024.
-
LICS Test-of-Time Award Winner in 2023
All papers from LICS 2003 were considered for the 2023 LICS Test-of-Time Award. The Award Committee consisted of Nathalie Bertrand, Phokion G. Kolaitis (chair), John Mitchell.
Constraint satisfaction problems constitute a large family of ubiquitous algorithmic problems that contain Boolean satisfiability and graph colorability as special cases. In 1993, Tomas Feder and Moshe Vardi conjectured that for every relational structure B, the associated constraint satisfaction problem CSP(B) is either NP-complete or solvable in polynomial time. The Feder-Vardi conjecture became the catalyst for numerous subsequent investigations aiming to classify the complexity of constraint satisfaction problems. Andrei Bulatov's paper confirmed the Feder-Vardi conjecture for the case of conservative constraint satisfaction problems, which are the CSP(B) problems in which the relations in B include all subsets of the universe of B. This paper remained the strongest positive partial result towards the Feder-Vardi conjecture until the conjecture was finally proved independently by Andrei Bulatov and Dmitriy Zhuk in 2017 using methods and techniques from universal algebra.
Yannick Chevalier Ralf Küsters Michaël Rusinowitch Mathieu Turuani
An NP Decision Procedure for Protocol Insecurity with XORMore Information...Cryptographic protocols rely on cryptographic primitives to achieve goals such as data privacy and data authenticity in the presence of an attacker. Their use in important applications such as communications over the Internet or credit card payments calls for the automated verification of their security. These two papers made important progress on algorithmic aspects of protocol verification with additional operators, including XOR which is widely used in real-life applications. Specifically, these papers establish the decidability of insecurity of cryptographic protocols with XOR and other equational theories. Chevalier et al. prove membership in NP when restricted to XOR, while Comon and Shmatikov prove decidability in a broader setting. In addition to definitively settling the complexity question for these cases, the lasting value of this line of work is demonstrated by mature verification tools such as ProVerif, Tamarin, Maude-NPA, and CPSA.
Hubert Comon-Lundh Vitaly Shmatikov
Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive orMore Information...Cryptographic protocols rely on cryptographic primitives to achieve goals such as data privacy and data authenticity in the presence of an attacker. Their use in important applications such as communications over the Internet or credit card payments calls for the automated verification of their security. These two papers made important progress on algorithmic aspects of protocol verification with additional operators, including XOR which is widely used in real-life applications. Specifically, these papers establish the decidability of insecurity of cryptographic protocols with XOR and other equational theories. Chevalier et al. prove membership in NP when restricted to XOR, while Comon and Shmatikov prove decidability in a broader setting. In addition to definitively settling the complexity question for these cases, the lasting value of this line of work is demonstrated by mature verification tools such as ProVerif, Tamarin, Maude-NPA, and CPSA.
The presentation of the award took place at LICS 2023.
-
LICS Test-of-Time Award Winner in 2022
All papers from LICS 2002 were considered for the 2022 LICS Test-of-Time Award. The Award Committee consisted of Joel Ouaknine (chair), Orna Grumberg, and Alexandra Silva.
Josée Desharnais Vineet Gupta Radha Jagadeesan Prakash Panangaden
The Metric Analogue of Weak Bisimulation for Probabilistic ProcessesMore Information...Bisimulation is a fundamental observational equivalence on labelled transition systems, first defined by Park and Milner in the 1980s. The present paper studies finite-state probabilistic automata, representing them as alternating automata. Here probabilistic transitions alternate with nondeterministic transitions: a probabilistic transition from a state ends in a set of possible states, and a nondeterministic choice – selected by a scheduler – determines the state on which to apply the next probabilistic transition. The fundamental insight is the definition of a pseudometric in which states at distance zero from one another are exactly those that are weakly bisimilar. Moreover, states that are close to one another have observable properties that also are close to one another. A partial order is defined on the pseudometrics on such a system, under which the pseudometric characterizing weak bisimilarity is the greatest fixed point of a particular operator. This greatest fixed point also is shown to be the solution to a linear programming problem, whose dual problem supports the application of conductive principles to reason about these structures. The fact that the observable properties are close if the states are close in the pseudometric allows results about Markov chains to be established in this setting. This landmark paper is a tour de force, applying new techniques in novel ways to support what constitutes groundbreaking research into how to analyse probabilistic processes and their applications, in varied domains such as security (including privacy and information flow), fuzzy systems, control systems, mobile process theory, software engineering, programming language theory, formal methods, and coalgebraic process theory, among others.
François Laroussinie Nicolas Markey Philippe Schnoebelen
Temporal Logic with Forgettable PastMore Information...This extraordinarily clear and elegant paper provides well-motivated and complete characterisations of succinctness and complexity of linear temporal logic with past operators and with forgettable past. It has contributed to spur a vibrant research programme on logics and automata over infinite alphabets, from hardness results to the translations of logical formulas into alternating register automata, along with the attendant powerful algorithmic consequences for model checking. It has also strongly influenced the development of the field of nominal computation, and it is no exaggeration to state that the present paper has tangibly led to a number of invited talks, Dagstuhl-type workshops, research grants, academic positions, and prizes, and continues to have an ongoing and lasting impact in the areas of automata theory and the foundations of automated verification.
The presentation of the award took place at LICS 2022.
-
LICS Test-of-Time Award Winner in 2021
All papers from LICS 2001 were considered for the 2021 LICS Test-of-Time Award. The Award Committee consisted of Parosh Abdulla, Manuel Bodirsky (chair), Erich Graedel, and Radha Jagadeesan.
Verification of Program termination is of significant practical importance. In this paper, Xi describes a dependent type system that enables the programmer to supply metrics for verifying program termination, in order to establish the guarantee that every well-typed program in this type system is terminating. The type system of the paper supports a general form of recursion, higher-order functions, algebraic datatypes, and polymorphism. Thus, it advances the hope of incorporating the rich body of literature on proving termination into a realistic functional programming language. The promise of this paper has been realised in subsequent research in various research groups. It has also impacted publicly available tools such as LiquidHaskell, a library for general purpose programs in Haskell.
The presentation of the award took place at LICS 2021.
-
LICS Test-of-Time Award Winner in 2020
All papers from LICS 2000 were considered for the 2020 LICS Test-of-Time Award. The Award Committee consisted of Thierry Coquand (chair), Pierre-Louis Curien, Marcelo Fiore, and Orna Kupferman.
The setting of two player games on finite graphs, used to model interactions between systems and their environments, has been extensively studied in the context of synthesis and control. A key issue for concurrent games is that it requires probabilistic considerations. This paper handled concurrent games with omega-regular objectives (that is, the winning condition refers to the infinite path that the players generate). It studied the theoretical properties of the games and provided clever algorithms for computing the sets of winning states for three different qualitative modes of winning, reflecting different probabilistic guarantees. By settling several fundamental results of this theory, this is a landmark paper that has been extended to include further qualitative parameters (energy and other weighted games), richer winning conditions, and applications beyond traditional synthesis and control.
This paper brought new light to the study of equi-recursive types in the context of the propositions-as-types paradigm; especially to arbitrary recursive types, such as the famous equation D = D -> D underlying the semantics of the untyped lambda-calculus, as well as self-referential types featuring in object-oriented programming. Roughly, the key idea is to have a stratified view of such types reflecting more and more precise properties that correspond to iterations of an associated induction step. The paper puts forward this approach and, importantly, formalizes it by means of a very natural modality that shifts the stratification. The resulting system allows a kind of guarded approach to general recursion that can avoid the pitfalls of non-termination getting in the way of formal reasoning. The work connected recursion with the methods of Kripke and realizability semantics, belonging to the realm of intuitionistic logic, and, yet to be further explored, to provability logic. These ideas and techniques are now widespread and popular in step-indexed logical relations and in various modal extensions of type theory that are under active investigation.
The presentation of the award took place at LICS 2020.
-
LICS Test-of-Time Award Winner in 2019
All papers from LICS 1999 were considered for the 2019 LICS Test-of-Time Award. The Award Committee consisted of Thomas Ehrhard, Frank Pfenning (chair), and Davide Sangiorgi.
Marcelo P. Fiore Gordon D. Plotkin Daniele Turi
Abstract Syntax and Variable BindingMore Information...Variable binding operators are pervasive in the study of programming languages and logics. Following an idea of Church (1940) these can be reduced to a single binding operator whose syntactic properties have been understood for some time. These two seminal papers propose contrasting approaches to achieve a matching semantic understanding for abstract syntax with binding. Gabbay and Pitts employ the permutation model of set theory with atoms due to Fraenkel and Mostowski to represent name abstraction and fresh name generation. This led to a wealth of research using so-called nominal techniques, both in theory and in practical implementations in theorem provers. An extended and revised version of their paper was published in Formal Aspects of Computing in 2002. Fiore, Plotkin, and Turi instead take a categorical approach, devising binding algebras that are presheaves endowed with both an algebra structure and a substitution structure that are compatible with each other. Abstract syntax with binding is then an initial model. The compatibility of this idea with de Bruijn indices, already popular in formal developments before 1999, has led to many applications of their results in further theory and implementations.
Murdoch Gabbay Andrew M. Pitts
A New Approach to Abstract Syntax Involving BindersMore Information...Variable binding operators are pervasive in the study of programming languages and logics. Following an idea of Church (1940) these can be reduced to a single binding operator whose syntactic properties have been understood for some time. These two seminal papers propose contrasting approaches to achieve a matching semantic understanding for abstract syntax with binding. Gabbay and Pitts employ the permutation model of set theory with atoms due to Fraenkel and Mostowski to represent name abstraction and fresh name generation. This led to a wealth of research using so-called nominal techniques, both in theory and in practical implementations in theorem provers. An extended and revised version of their paper was published in Formal Aspects of Computing in 2002. Fiore, Plotkin, and Turi instead take a categorical approach, devising binding algebras that are presheaves endowed with both an algebra structure and a substitution structure that are compatible with each other. Abstract syntax with binding is then an initial model. The compatibility of this idea with de Bruijn indices, already popular in formal developments before 1999, has led to many applications of their results in further theory and implementations.
The presentation of the award took place at LICS 2019.
-
LICS Test-of-Time Award Winner in 2018
All papers from LICS 1998 were considered for the 2018 LICS Test-of-Time Award. The Award Committee consisted of Christel Baier (chair), Luca Aceto, Anca Muscholl, and Vaughan Pratt.
Martín Abadi Cédric Fournet Georges Gonthier
Secure Implementation of Channel AbstractionsMore Information...A secure channel is an important primitive in distributed systems programming. It protects the confidentiality of messages while they traverse untrusted networks. It is folklore that a secure channel can be implemented using cryptography, specifically using encryption. However, it is the LICS 1998 paper “Secure Implementation of Channel Abstractions” that formalizes this folklore idea and shows howto mathematically specify that a secure channel has been implemented correctly. In doing so, the paper also demonstrates, for the first time, how the classic concept of full abstraction of language translations can be used to formalize the preservation of security properties, an idea that has been used several times subsequently.
Samson Abramsky Kohei Honda Guy McCusker
A Fully Abstract Game Semantics for General ReferencesMore Information...This paper presented the first games model of a programming language with higher-order store a la ML references. The result came as a big surprise within the community at the time and was a technical tour de force. Seen from today’s perspective, the article was certainly one of the main achievements of game semantics, and extended the reach of games models well beyond the work on PCF by Nickau, Hyland and Ong, and Abramsky, Jagadeesan and Malacaria (which received the 2017 Alonzo Church Award). The paper also opened a new field of research, which is still being explored and exploited today within the game-semantics community.
The presentation of the award took place at LICS 2018.
-
LICS Test-of-Time Award Winner in 2017
All papers from LICS 1997 were considered for the 2017 LICS Test-of-Time Award. The Award Committee consisted of Amy Felty (chair), Christel Baier, Andrew Pitts, and Nicole Schweikardt.
Richard Blute Josée Desharnais Abbas Edalat Prakash Panangaden
Bisimulation for Labelled Markov ProcessesMore Information...The paper introduces labelled Markov processes as a continuous- space variant of deterministic labeled transition systems where the dynamics of the state-action pairs is given by Markov kernels specifying the probability for measurable sets of successor states. The presented notion of bisimulation of labelled Markov processes is a conservative extension of Larsen and Skou’s bisimulation for discrete probabilistic transition systems. The paper presents a highly non-trivial proof for the transitivity of bisimulation on labelled Markov processes and first steps towards a logical characterization of bisimulation in terms of a probabilistic Hennessy-Milner logic. By introducing labeled Markov processes and a notion of bisimulation for them, the authors provided important foundations for the formal semantics and analysis of stochastic systems where physical components interact with discrete ones. The paper opened a new research area on continuous-space stochastic models and inspired many researchers to study further properties of labelled Markov processes and variants thereof.
This paper introduced a new and mathematically elegant way of relating the syntax and semantics of programs, using the existing category-theoretic notion of a distributive law between monads and comonads. Specifically, it gives an abstract view of the structural operational semantics of concurrent processes as distributing behaviour over syntax, one which guarantees the existence of a most abstract, compositional semantics of the language. The paper was an early example of the usefulness of coalgebraic techniques in semantics and has been, and still is, an extremely influential paper within the coalgebra community.
The presentation of the award took place at LICS 2017.
-
LICS Test-of-Time Award Winner in 2016
All papers from LICS 1996 were considered for the 2016 LICS Test-of-Time Award. The Award Committee consisted of Amy Felty, Jean-Pierre Jouannaud (chair), Naoki Kobayashi, and Glynn Winskel.
Parosh A. Abdulla Karlis Cerans Bengt Jonsson Yih-Kuen Tsay
General decidability theorems for infinite-state systemsMore Information...The LICS-1996 paper "General decidability theorems for infinite-state systems" authored by Abdulla, Cerans, Jonsson and Tsay showed that various verification problems are decidable for well-structured transition systems (WSTS). WSTS is a general class of infinite systems that subsumes a number of important computation models such as Petri nets and lossy channel systems. While the notion of WSTS was introduced in 1990 by Finkel with a slightly restricted format, the present paper proved the decidability of the coverability problem for the general class introduced there by describing a backward algorithm. This powerful technique has been quite influential in the field, and cited ever since as a standard reference on WSTS.
The Linear Logical Framework (LLF) presented in the LICS 1996 paper "A Linear Logic Framework" authored by Cervesato and Pfenning was one of the first logical frameworks to build the notion of linearity directly into the framework, and the first one to do so using a dependently-typed lambda-calculus in the style of Harper, Honsell, and Plotkin's Logical Framework (LF). As a result, the meta-theory of a variety of logical formalisms such as imperative programming languages can be elegantly formalized, with concepts such as program state more directly and concisely encoded using the linear features. The impact of this work continues as newer application areas such as quantum programming languages benefit from the availability of this kind of framework. In addition, this work continues to be influential in the development of new frameworks, such as those with richer dependently-typed calculi, which build on the foundations established in this paper.
The presentation of the award took place at LICS 2016.
-
LICS Test-of-Time Award Winner in 2015
All papers from LICS 1995 were considered for the 2015 LICS Test-of-Time Award. The Award Committee consisted of Martin Grohe, Dexter Kozen, Dale Miller (Chair) and Prasad Sistla.
Igor Walukiewicz
Completeness of Kozen's Axiomatisation of the Propositional Mu-CalculusMore Information...The propositional mu-calculus (now more commonly known as the modal mu-calculus) was first published in 1983 by D. Kozen, although the system had been studied much earlier by J. de Bakker and D. Scott (unpublished notes, 1969). The system subsumes many popular propositional logics of programs, including linear temporal logic, computation tree logic CTL*, and propositional dynamic logic. Kozen proposed a deductive system whose chief rule of inference was a variant of the fixpoint induction rule of D. Park and conjectured it to be complete. During the decade after its introduction, this calculus attracted a great deal of attention within computer science circles. Despite the attention given to this calculus, it was not until this paper by Walukiewicz a dozen years later that the proof system was finally shown to be complete. In order to prove the completeness theorem, several technical innovations were developed. A full version of this paper appeared in Information and Computation in 2000.
The presentation of the award took place at LICS 2015.
-
LICS Test-of-Time Award Winner in 2014
All papers from LICS 1994 were considered for the 2014 LICS Test-of-Time Award. The Award Committee consisted of Thierry Coquand, Dexter Kozen (chair), Leonid Libkin and Frank Pfenning. Two awards were made.
Martin Hofmann Thomas Streicher
The groupoid model refutes uniqueness of identity proofsMore Information...This paper opened a series of investigations leading to the development of homotopy type theory, an area of intense current research that touches on the very foundations of the field. The paper contained two key insights: first, that it follows from the rules of type theory that types have a groupoid structure; and second, that groupoids form a model of type theory. The results were quite surprising at the time and opened up a new front in the quest to understand the tradeoffs between intensional and extensional type theory. Although later revised and extended by the authors and others, the original insights were in the original LICS paper and were an essential forerunner of more recent develop- ments on univalent foundations that led to homotopy type theory in its present form.
Jean-Yves Girard had introduced linear logic about seven years prior to the appearance of this paper and, in several subsequent papers, cemented its role as a quintessential, unifying logic. In this 1994 LICS paper, Miller showed that linear logic could also be used as a logical framework, providing means for the elegant, high-level representation of formal systems. Miller gives examples from the domains of logic (natural deduction) and programming languages (opera- tional semantics, including effects). This appropriated linear logic for purposes of practical specifications of stateful and concurrent systems. This work has been quite influential over the years and even up to the present with the cur- rently active area of behavioral types.
The presentation of the awards took place at CSL-LICS 2014.
-
LICS Test-of-Time Award Winner in 2013
All papers from LICS 1993 were considered for the 2013 LICS Test-of-Time Award. The Award Committee consisted of Jean-Pierre Jouannaud, Martin Grohe, Tom Henzinger, and Prakash Panangaden (chair). Three papers have been selected.
This paper introduces a general framework for solving set constraints which were introduced earlier in a logic programming setting by Jaffer and Heintze. While others had used specialized tools to attack this problem the approach of this paper remains fundamental shedding light on the significance of the monadic class. They showed that the satisfiability problem for set con- straints is complete for NEXPTIME and obtained many decidability and complexity results for extensions of set constraints. Though there have been many extensions this paper remains the reference on the topic.
Bisimulation had been for about 20 years a central concept in concurrency theory when this paper appeared. However, there were numerous variations and adaptations for different types of systems. This paper presented a very abstract and general definition that applied across a large class of systems and which easily specializes to many cases such as Milner’s strong bisim- ulation, history-preserving bisimulation. This paper was the precursor to many later papers on presheaf models for concurrency. This was expressed in the original paper as a promising line of future research and was spectacularly vindicated in subsequent years largely through the work of Winskel and his collaborators. It even served as the inspiration for future work on probabilistic bisimulation though that was not realized at the time.
This paper marks the beginning of a very successful fusion of ideas from type theory and concurrency. Milner’s π-calculus from the late 1980s was a pioneering example of a mobile calculus and initiated a new direction of research in concurrency theory. Milner’s original type discipline for this calculus was rudimentary. Pierce and Sangiorgi introduced a more refined type system that distinguishes between different ways in which a process can access a channel. This leads to a natural subtype relation between processes and to stronger theorems about the encodings of the λ-calculus into the π-calculus. This highly cited paper is the inspiration for many later typed mobile calculi.
The presentation of the awards will take place at LICS 2013.
-
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.