www.wikidata.de-de.nina.az

Peter W O Hearn 13 Juli 1963 in Halifax Nova Scotia ist ein kanadischer Informatiker studierte Informatik an der Dalhous

Peter W. O’Hearn

Peter W. O’Hearn (* 13. Juli 1963 in Halifax (Nova Scotia)) ist ein kanadischer Informatiker.

Peter W. O’Hearn

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. 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 Bearbeiten

  • 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

Weblinks Bearbeiten

Einzelnachweise Bearbeiten

  1. Laudatio Gödelpreis 2016
Personendaten
NAME O’Hearn, Peter W.
KURZBESCHREIBUNG kanadischer Informatiker
GEBURTSDATUM 13. Juli 1963
GEBURTSORT Halifax
wikipedia, wiki, deutsches, deutschland, buch, bücher, bibliothek artikel lesen, herunterladen kostenlos kostenloser herunterladen, MP3, Video, MP4, 3GP, JPG, JPEG, GIF, PNG, Bild, Musik, Lied, Film, Buch, Spiel, Spiele
Veröffentlichungsdatum:
Peter W O Hearn 13 Juli 1963 in Halifax Nova Scotia ist ein kanadischer Informatiker Peter W O HearnPeter 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 Universitat 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 ubernommen wurde arbeitet er seit 2013 auch als Engineering Manager fur 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 fur die Analyse und Verifizierung von Programmen entwickelt 2016 erhielt er mit Stephen Brookes von der Carnegie Mellon University den Godel Preis fur ihre Entwicklung der Concurrent Separation Logic CSL das nach der Laudatio ein revolutionarer Fortschritt bei Beweissystemen fur die Verifizierung von Eigenschaften von Systemsoftware war wozu typischerweise sowohl die Manipulation von Zeigern als auch die Verwaltung von Nebenlaufigkeit im gemeinsam von den Prozessen geteilten Speicher gehoren 1 Automatisierte Programm Verifizierer bestanden zuvor im Wesentlichen nur fur sequentielle Programme ohne Nebenlaufigkeit 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 Nebenlaufigkeit war fur die erste Ansatze von Susan Owicki und David Gries 1976 stammten durch Ubertragung des Hoare Kalkuls auf Parallelprogramme O Hearn befasst sich auch mit Internet Sicherheit 2007 erhielt er den Royal Society Wolfson Research Merit Award Schriften Bearbeitenmit 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 pdfWeblinks BearbeitenHomepageEinzelnachweise Bearbeiten Laudatio Godelpreis 2016Normdaten Person GND 17307538X lobid OGND AKS LCCN n96097208 VIAF 188793539 Wikipedia Personensuche PersonendatenNAME O Hearn Peter W KURZBESCHREIBUNG kanadischer InformatikerGEBURTSDATUM 13 Juli 1963GEBURTSORT Halifax Abgerufen von https de wikipedia org w index php title Peter W O Hearn amp oldid 178452266