Stephen Brookes

from Wikipedia, the free encyclopedia

Stephen D. Brookes , also Steve Brookes, is a computer scientist.

Brookes received his bachelor's degree in mathematics from Oxford University and received his doctorate there in 1983 with Tony Hoare in computer science (A Model for Communicating Sequential Processes). He has been at Carnegie Mellon University since 1981 , where he received a full professorship in 2006.

With Hoare and Bill Roscoe he developed the failures model of Communicating Sequential Processes (CSP), which he had introduced in his dissertation, improved it with Roscoe and which became the basis for the FDR (Failure Divergence Refinement) Model Checker. He dealt with semantic models for programming languages ​​with concurrent processes (such as Idealized CSP, Parallel Algol) and with intensional semantics .

In 2016, he and Peter W. O'Hearn received the Gödel Prize for their development of the Concurrent Separation Logic (CSL), which, according to the laudation, was a revolutionary advance in evidence systems for the verification of properties of system software, which typically includes the manipulation of pointers as well as the management of concurrency in the memory shared by the processes.

Web links

Individual evidence

  1. Laudation Gödel Prize 2016