Peter W. O'Hearn
Peter W. O'Hearn (born July 13, 1963 in Halifax (Nova Scotia) ) is a Canadian computer scientist.
Peter W. O'Hearn studied computer science at Dalhousie University in Halifax with a bachelor's degree in 1985 and at Queen's University (Kingston) with a master's degree in 1987. He received his doctorate there in 1991 under Robert D. Tennent (Semantics of Non- interference: A natural approach). Stephen Brookes was the external reviewer . From 1990 he was Assistant Professor at Syracuse University and from 1996 Reader and from 1999 Professor at Queen Mary College of the University of London and has been Professor at University College London on a Royal Academy of Engineering / Microsoft Research Chair since 2012 . After his startup company Monoidics was taken over by Facebook , he has also been working as an engineering manager for Facebook in London since 2013.
In 2006 he was visiting scholar at Microsoft Research in Cambridge and in 1997 visiting scholar at Carnegie Mellon University .
O'Hearn deals with logic and programming languages, doing basic theoretical research as well as developing practical software tools for the analysis and verification of programs.
In 2016, he and Stephen Brookes from Carnegie-Mellon University 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, typically including manipulation of pointers as well as the management of concurrency in the memory shared by the processes. Automated program verifiers previously existed essentially only for sequential programs without concurrency. O'Hearn had started development around 2002, having previously worked with John Reynolds and others to make advances in separation logics in the handling of pointers in sequential programs, and this was also one of the major obstacles in the development of program verification in concurrency (for the first Approaches by Susan Owicki and David Gries 1976 came from applying the Hoare calculus to parallel programs ).
O'Hearn also deals with internet security.
In 2007 he received the Royal Society Wolfson Research Merit Award.
Fonts
- with Steve Brookes: Concurrent Separation Logic, ACM SIGLOG News, Volume 3, No. 3, 2016, pp. 47-65, pdf
- with Samin Ishtiaq: BI as an assertion language for mutable data structures, Proceedings of the 28th Symposium on Principles of Programming Languages (POPL) 2001, pp. 36–49 (the work won the Most Influential POPL Paper Award in 2011)
- with H. Yang, JC Reynolds: Local Reasoning about Programs that Alter Data Structures, 15. Annual Conference of the European Association for Computer Science Logic (CSL) 2001, pp. 1-19
- with Cristiano Calcagno, Dino Distefano, Hongseok Yang: Compositional Shape Analysis by means of Bi-Abduction, Journal of the Association for Computing Machinery, Volume 58, Issue 6, 2011
- Resources, concurrency and local reasoning, Theoretical Computer Science, Volume 375, 2007, pp. 271-307
- with H. Yang, JC Reynolds: Separation and information hiding, ACM TOPLAS, Volume 31, No. 3, 2009
- A primer of separation logic, in: Software safety and security, NATO Science for Peace and Security Series, Volume 33, 2012, pp. 286-313, pdf
Web links
Individual evidence
| personal data | |
|---|---|
| SURNAME | O'Hearn, Peter W. |
| BRIEF DESCRIPTION | Canadian computer scientist |
| DATE OF BIRTH | July 13, 1963 |
| PLACE OF BIRTH | Halifax |