Dr. Stephen Brookes

Biography

Stephen Brookes is known internationally for his seminal contributions to the semantics of concurrent programs and the logics of reasoning about program behaviour. He earned his bachelor’s degree in Mathematics and Ph.D. in Computer Science from Oxford University. He joined Carnegie Mellon University as a research computer scientist in 1981 and became a full professor in 2006. His doctoral dissertation, supervised by Tony Hoare, was titled "A Model of Communicating Sequential Processes". His collaboration with Bill Roscoe led to the development of the failures-divergences model of CSP. Over the years, Brookes has developed a trace-based framework for providing semantics across a range of parallel paradigms, including shared-memory and both synchronous and asynchronous communication. His work on Parallel Algol demonstrates how these ideas can be extended to deal with languages that combine concurrency with higher-order procedures. His long-term research aim is to improve the design and analysis of correct concurrent programs. Recently, his joint work with Peter O’Hearn on Concurrent Separation Logic represents a major development direction, supporting correctness proofs for software that involves pointer manipulation in shared-memory concurrency. This work has had a significant impact both in theory and practice. Brookes and O’Hearn were awarded the 2016 Gödel Prize by the European Association for Theoretical Computer Science and the ACM Special Interest Group on Algorithms and Computation Theory (ACM SIGACT).

Research Interests