Peter W. O’Hearn
Peter W. O’Hearn (* 13. Juli 1963 in Halifax (Nova Scotia)) ist ein kanadischer Informatiker.
Peter W. O’Hearn studierte Informatik an der Dalhousie University in Halifax mit dem Bachelor-Abschluss 1985 und an der Queen’s University (Kingston) mit dem Master-Abschluss 1987. Er wurde dort 1991 bei Robert D. Tennent promoviert (Semantics of Non-interference: A natural approach). Externer Gutachter war dabei Stephen Brookes. Ab 1990 war er Assistant Professor an der Syracuse University und ab 1996 Reader und ab 1999 Professor am Queen Mary College der Universität London und ist seit 2012 Professor am University College London auf einem Royal Academy of Engineering/Microsoft Research Chair. Nachdem sein Startup-Unternehmen Monoidics von Facebook übernommen wurde arbeitet er seit 2013 auch als Engineering Manager für Facebook in London.
2006 war er Gastwissenschaftler bei Microsoft Research in Cambridge und 1997 Gastwissenschaftler an der Carnegie Mellon University.
O’Hearn befasst sich mit Logik und Programmiersprachen, wobei er sowohl theoretische Grundlagenforschung betreibt als auch praktische Softwaretools für die Analyse und Verifizierung von Programmen entwickelt.
2016 erhielt er mit Stephen Brookes von der Carnegie-Mellon University den Gödel-Preis für ihre Entwicklung der Concurrent Separation Logic (CSL), das nach der Laudatio ein revolutionärer Fortschritt bei Beweissystemen für die Verifizierung von Eigenschaften von Systemsoftware war, wozu typischerweise sowohl die Manipulation von Zeigern als auch die Verwaltung von Nebenläufigkeit im gemeinsam von den Prozessen geteilten Speicher gehören.[1] Automatisierte Programm-Verifizierer bestanden zuvor im Wesentlichen nur für sequentielle Programme ohne Nebenläufigkeit. O´Hearn hatte um 2002 mit der Entwicklung begonnen, nachdem er zuvor mit John Reynolds und anderen Fortschritte mit Separationslogiken bei der Behandlung von Zeigern in sequentiellen Programmen erzielt hatte und dies auch einer der Haupthindernisse in der Entwicklung von Programmverifizieren bei Nebenläufigkeit war (für die erste Ansätze von Susan Owicki und David Gries 1976 stammten durch Übertragung des Hoare-Kalküls auf Parallelprogramme).
O´Hearn befasst sich auch mit Internet-Sicherheit.
2007 erhielt er den Royal Society Wolfson Research Merit Award.
Schriften
- mit Steve Brookes: Concurrent Separation Logic, ACM SIGLOG News, Band 3, Nr. 3, 2016, S. 47–65, pdf
- mit Samin Ishtiaq : BI as an assertion language for mutable data structures, Proceedings of the 28. Symposium on Principles of Programming Languages (POPL) 2001, S. 36–49 (die Arbeit gewann 2011 den Most Influential POPL Paper Award)
- mit H. Yang, J. C. Reynolds: Local Reasoning about Programs that Alter Data Structures,15. Annual Conference of the European Association for Computer Science Logic (CSL) 2001, S. 1–19
- mit Cristiano Calcagno, Dino Distefano, Hongseok Yang: Compositional Shape Analysis by means of Bi-Abduction, Journal of the Association for Computing Machinery, Band 58, Heft 6, 2011
- Resources, concurrency and local reasoning, Theoretical Computer Science, Band 375, 2007, S. 271–307
- mit H. Yang, J.C. Reynolds: Separation and information hiding, ACM TOPLAS, Band 31, Nr. 3, 2009
- A primer of separation logic, in: Software safety and security, NATO Science for Peace and Security Series, Band 33, 2012, S. 286–313, pdf