Some Recent Awards

A few awards and prizes have recently been handed out to members of the TCS community.

The LICS test-of-time award 2008 has been given to Martín Abadi and Leslie Lamport for their paper The Existence of Refinement Mappings. In Lamport's own words:

The method of proving that one specification implements another by using a refinement mapping was well-established by the mid-80s. ..... It was known that constructing the refinement mapping might require adding history variables to the implementation. Indeed, Lam and Shankar essentially constructed all their refinement mappings with history variables. Jim Saxe discovered a simple example showing that history variables weren't enough. To handle that example, he devised a more complicated refinement-mapping rule. I realized that I could eliminate that complicated rule, and use ordinary refinement, by introducing a new kind of dummy variable that I called a prophecy variable. A prophecy variable is very much like a history variable, except it predicts the future instead of remembering the past. (Nancy Lynch later rediscovered Saxe's rule and used it to "simplify" refinement proofs by eliminating prophecy variables.) I then remembered a problematic example by Herlihy and Wing in their classic paper Linearizability: A Correctness Condition for Concurrent Objects that could be handled with prophecy variables.

This paper was my first collaboration with Abadi. Here's my recollection of how it was written. I had a hunch that history and prophecy variables were all one needed. Abadi had recently joined SRC, and this seemed like a fine opportunity to interest him in the things I was working on. So I described my hunch to him and suggested that he look into proving it. He came back in a few weeks with the results described in the paper. My hunch was right, except that there were hypotheses needed that I hadn't suspected. Abadi, however, recalls my having had a clearer picture of the final theorem, and that we worked out some of the details together when writing the final proof.

I had just developed the structured proof style described in [100], so I insisted that we write our proofs in this style, which meant rewriting Abadi's original proofs. In the process, we discovered a number of minor errors in the proofs, but no errors in the results.

The first CAV award has just been given to Rajeev Alur and David Dill for the invention of the formalism of timed automata. See the full announcement for more details. This is a well deserved recognition to Rajeev and David for a fundamental contribution to the theory of real-time systems verification. Timed automata have been the subject of extensive theoretical investigation since the original paper by Rajeev and David and form the basis for software tools for the specification and verification of real-time systems such as Uppaal. Readers who are interested in a leisurely introduction to the basic theory of timed automata might wish to read part II of this book.

Finally, the European Mathematical Society (EMS) awarded its prizes at the 5th European Congress of Mathematics, held this week in Amsterdam (The Netherlands). The EMS prizes are awarded to young researchers not older than 35 years, in recognition of distinguished contributions in mathematics, and are presented every four years at the European Congress of Mathematics. One of the recipients of the EMS prizes is Assaf Naor, who is honoured for "his groundbreaking contributions to functional analysis, the theory of algorithms, and combinatorics".

Congrats to the award recipients!