Stephen Brookes

Stephen Brookes is a Professor Emeritus in the Computer Science Department at Carnegie Mellon University. His research focuses on Programming Languages, with particular emphasis on Formal Methods, Pure and Applied Logic, and the semantics of concurrent programs. Brookes is well known for his contributions to the semantics of concurrent systems and the development of logics for reasoning about program behavior. His work includes the failures-divergences model of CSP and Concurrent Separation Logic, which has had significant impact in both theory and practice. He has collaborated with Peter O’Hearn on Concurrent Separation Logic, which supports correctness proofs for software involving pointer manipulation and shared-memory concurrency. Brookes has also worked on partial-order semantic models for relaxed memory concurrency. His research interests include the mathematical semantics of programming languages, intensional semantic models, and the design of programming languages that embody parallelism uniformly.