|2016 Gödel Prize|
The 2016 Gödel Prize is awarded to Stephen Brookes and Peter W. O'Hearn for their invention of Concurrent Separation Logic, as described in the following two papers:
Stephen Brookes and Peter O'Hearn will receive the 2016 Gödel Prize at the 43rd International Colloquium on Automata, Languages and Programming (ICALP 2016), 12-15 July 2016, in Rome, Italy.
Concurrent Separation Logic (CSL) is a revolutionary advance over previous proof systems for verifying properties of systems software, which commonly involve both pointer manipulation and shared-memory concurrency. For the last thirty years experts have regarded pointer manipulation as an unsolved challenge for program verification and shared-memory concurrency as an even greater challenge. Now, thanks to CSL, both of these problems have been elegantly and efficiently solved; and they have the same solution. Brookes and O'Hearn's approach builds on the Separation Logic for sequential programs due to O'Hearn and the late John Reynolds. The extension to treat concurrently executing programs communicating via shared state is highly non-trivial and involves a dynamic notion of resource ownership that supports modular reasoning. O'Hearn's initial proposals were shown to be unsound by an example due to Reynolds. O'Hearn and Brookes regained soundness by requiring certain assertions in the proof rules to be "precise" -- to unambiguously pick out an area of storage. O'Hearn's paper introduces CSL and is very much about fluency with the logic, how to reason with it, rather than its meta-theory. The latter is the concern of Brookes' paper, which demonstrates soundness of the logic via a clever new model; this was essential for CSL to be widely accepted and applied.
CSL’s impact has been extraordinary in both theoretical and practical realms. In the theoretical realm, almost all research papers developing concurrent program logics in the last decade are based on CSL, including work on permissions, refinement and atomicity, on adaptations to assembly languages and weak memory models, on higher-order variants, and on logics for termination of concurrent programs. In the practical realm, the beauty of CSL is in its similarity to the programming idioms commonly used by working engineers. The fact that the logic matches the common programming idioms has the effect of greatly simplifying proofs; with CSL many simple proofs are known now for programs where previously proofs were either complex or unknown. CSL's simplicity and structure also facilitates automation. As a result numerous tools and techniques in the research community are based on it and it is attracting attention in companies such as Microsoft, Facebook and Amazon.
Stephen Brookes is Professor of Computer Science at Carnegie Mellon University. He obtained his BA degree in Mathematics (1978) and his PhD degree in Computer Science (1983), both from Oxford University. His PhD thesis introduced the "failures" model of Hoare's CSP. A long-term aim of his research, culminating in his foundational work for Concurrent Separation Logic, has been to facilitate the design and analysis of correct concurrent programs. He has recently begun working on semantic models for weak memory concurrency. His work on Concurrent Separation Logic was partially funded by NSF.
Peter W. O'Hearn is an Engineering Manager at Facebook and a Professor of Computer Science at University College London. Previously he cofounded a verification startup, Monoidics, which was acquired by Facebook in 2013, and he has had academic positions at Queen Mary University of London and at Syracuse University. He is a past recipient of a Royal Society Wolfson Research Merit Award, a Most Influential POPL paper award, and a Royal Academy of Engineering/Microsoft Research Chair. He received his BSc degree from Dalhousie University (1985) and MSc and PhD degrees from Queen’s University (1987, 1991).
The Gödel Prize includes an award of USD 5,000, and is named in honor of Kurt Gödel, who was born in Austria-Hungary (now the Czech Republic) in 1906. Gödel's work has had immense impact upon scientific and philosophical thinking in the 20th century. The award recognizes his major contributions to mathematical logic and the foundations of computer science.
Gödel Prize committee:
Moses Charikar (Stanford University)
Orna Kupferman (Hebrew University)
Kurt Mehlhorn (Max Planck Institute)
Joe Mitchell (SUNY at Stony Brook)
Andrew Pitts (University of Cambridge, chair)
Madhu Sudan (Harvard University)