Jump to content

Peter O'Hearn: Difference between revisions

From Wikipedia, the free encyclopedia
Browse history interactively
← Previous editNext edit →
Content deleted Content added
VisualWikitext
Citation bot (talk | contribs)
Bots
5,408,160 edits
m Alter: title. Add: url, jstor, doi, journal. Removed parameters. Some additions/deletions were actually parameter name changes.| You can use this bot yourself. Report bugs here.| Activated by User:Nemo bis | via #UCB_webform
No edit summary
Line 47: Line 47:


==Career and research==
==Career and research==
O'Hearn is best known for [[separation logic]],<ref name="lics02">{{cite journal| url=https://www.cs.cmu.edu/~jcr/seplogic.pdf | title=Separation Logic: A Logic for Shared Mutable Data Structures | first=John C. | last=Reynolds | authorlink=John C. Reynolds | journal=LICS | year=2002 }}</ref> a theory he developed with [[John C. Reynolds]] that unearthed new domains for scaling logical reasoning about code. This built upon previous research from O'Hearn and David Pym on logic for resources — [[Bunched logic]].<ref name="bi">{{cite journal| title=The Logic of Bunched Implications | first1=P. W. | last1=O'Hearn | first2=D. J. | last2=Pym | journal=[[Bulletin of Symbolic Logic]] | volume=5 | number=2 |date=June 1999 | pages=215–244 | doi=10.2307/421090 | jstor=421090 | url=https://semanticscholar.org/paper/99ee6eb28490ffce90716365c4e0a3b1018738eb }}</ref>
O'Hearn is best known for [[separation logic]],<ref name="lics02">{{cite journal| url=https://www.cs.cmu.edu/~jcr/seplogic.pdf | title=Separation Logic: A Logic for Shared Mutable Data Structures | first=John C. | last=Reynolds | authorlink=John C. Reynolds | journal=LICS | year=2002 }}</ref> a theory he developed with [[John C. Reynolds]] that unearthed new domains for scaling logical reasoning about code. This built upon previous research from O'Hearn and David Pym on logic for resources — [[Bunched logic]].<ref name="bi">{{cite journal| title=The Logic of Bunched Implications | first1=P. W. | last1=O'Hearn | first2=D. J. | last2=Pym | journal=[[Bulletin of Symbolic Logic]] | volume=5 | number=2 |date=June 1999 | pages=215–244 | doi=10.2307/421090 | jstor=421090 | url=https://semanticscholar.org/paper/99ee6eb28490ffce90716365c4e0a3b1018738eb }}</ref> With Stephen Brookes, [[Carnegie Mellon University]], O'Hearn created, Concurrent Separation Logic (CSL), extending the theory further. [[Tony Hoare]], in discussing the grand challenge of program verification, described CSL as "solving two problems...concurrecy and object orientation".<ref>https://www.facebook.com/academics/videos/2228616734102290/?t=3775</ref> <ref>https://dl.acm.org/doi/10.1145/602382.602403</ref>


Separation logic has given rise to the [[Infer Static Analyzer]] (Facebook Infer), a [[static program analysis]] utility developed by O'Hearn's team at [[Facebook]].<ref name=fbinfer/> After 20 plus years in academia, O'Hearn landed at Facebook in 2013 with the acquisition of Monoidics Ltd, a startup he cofounded.<ref>{{cite web|url=https://techcrunch.com/2013/07/18/facebook-monoidics/|title=Facebook Acquires Assets Of UK Mobile Bug-Checking Software Developer Monoidics – TechCrunch|website=techcrunch.com}}</ref> Since its inception, Infer has enabled Facebook engineers to resolve tens of thousands of bugs before reaching production.<ref>{{cite web|url=https://research.fb.com/publications/continuous-reasoning-scaling-the-impact-of-formal-methods|title=Continuous Reasoning: Scaling the Impact of Formal Methods|website=Facebook Research}}</ref> It was open sourced in 2016, and is used by [[Amazon Inc]], [[Spotify]], [[Mozilla]], [[Uber]], and others.<ref name=fbinfer/> In 2017, O'Hearn and the team open sourced RacerD, an automated static race condition detection tool that reduces the time it takes to flag potential problems in concurrent software, as part of the Infer platform.<ref>{{cite news|url=https://www.techrepublic.com/article/facebook-open-sources-racerd-a-tool-thats-already-squashed-1000-bugs-in-concurrent-software/|title=Facebook open sources RacerD: A tool that's already squashed 1,000 bugs in concurrent code|date=19 October 2017|publisher=[[TechRepublic]]}}</ref>
Separation logic has given rise to the [[Infer Static Analyzer]] (Facebook Infer), a [[static program analysis]] utility developed by O'Hearn's team at [[Facebook]].<ref name=fbinfer/> After 20 plus years in academia, O'Hearn landed at Facebook in 2013 with the acquisition of Monoidics Ltd, a startup he cofounded.<ref>{{cite web|url=https://techcrunch.com/2013/07/18/facebook-monoidics/|title=Facebook Acquires Assets Of UK Mobile Bug-Checking Software Developer Monoidics – TechCrunch|website=techcrunch.com}}</ref> Since its inception, Infer has enabled Facebook engineers to resolve tens of thousands of bugs before reaching production.<ref>{{cite web|url=https://research.fb.com/publications/continuous-reasoning-scaling-the-impact-of-formal-methods|title=Continuous Reasoning: Scaling the Impact of Formal Methods|website=Facebook Research}}</ref> It was open sourced in 2016, and is used by [[Amazon Inc]], [[Spotify]], [[Mozilla]], [[Uber]], and others.<ref name=fbinfer/> In 2017, O'Hearn and the team open sourced RacerD, an automated static race condition detection tool that reduces the time it takes to flag potential problems in concurrent software, as part of the Infer platform.<ref>{{cite news|url=https://www.techrepublic.com/article/facebook-open-sources-racerd-a-tool-thats-already-squashed-1000-bugs-in-concurrent-software/|title=Facebook open sources RacerD: A tool that's already squashed 1,000 bugs in concurrent code|date=19 October 2017|publisher=[[TechRepublic]]}}</ref>

Revision as of 09:41, 1 January 2020

Peter O'Hearn
FRS FREng
Peter O'Hearn at the Royal Society admissions day in London, July 2018
Born
Peter William O'Hearn

13 July 1963 (1963-07-13) (age 61)
Halifax, Nova Scotia, Canada
NationalityBritish/Canadian
CitizenshipUnited Kingdom/Canada
Alma materDalhousie University (BSc)
Queen's University (MSc, PhD)
Known forSeparation logic[12]
Bunched logic[13]
Infer Static Analyzer[14]
Awards
Scientific career
FieldsProgramming languages[9]
Program analysis
Formal verification
Theoretical computer science[9]
InstitutionsFacebook
University College London
Queen Mary University of London
Syracuse University
ThesisSemantics of Non-interference: A natural approach (1992)
Doctoral advisorRobert D. Tennent[10]
Websitewww0.cs.ucl.ac.uk/staff/p.ohearn/

Peter William O'Hearn FRS FREng[4][6] (born 13 July 1963 in Halifax, Nova Scotia) is a research scientist at Facebook[15] and a Professor of Computer science at University College London (UCL).[16] He has made significant contributions to formal methods for program correctness. In recent years these advances have been employed in developing industrial software tools that conduct automated analysis of large industrial codebases.[9]

Education

O'Hearn attained a BSc degree in computer science from Dalhousie University, Halifax, Nova Scotia (1985), followed by MSc (1987) and PhD (1991) degrees from Queen's University, Kingston, Ontario, Canada. His dissertation was on Semantics of Non-interference: A natural approach, supervised by Robert D. Tennent.[10][17]

Career and research

O'Hearn is best known for separation logic,[12] a theory he developed with John C. Reynolds that unearthed new domains for scaling logical reasoning about code. This built upon previous research from O'Hearn and David Pym on logic for resources — Bunched logic.[13] With Stephen Brookes, Carnegie Mellon University, O'Hearn created, Concurrent Separation Logic (CSL), extending the theory further. Tony Hoare, in discussing the grand challenge of program verification, described CSL as "solving two problems...concurrecy and object orientation".[18] [19]

Separation logic has given rise to the Infer Static Analyzer (Facebook Infer), a static program analysis utility developed by O'Hearn's team at Facebook.[14] After 20 plus years in academia, O'Hearn landed at Facebook in 2013 with the acquisition of Monoidics Ltd, a startup he cofounded.[20] Since its inception, Infer has enabled Facebook engineers to resolve tens of thousands of bugs before reaching production.[21] It was open sourced in 2016, and is used by Amazon Inc, Spotify, Mozilla, Uber, and others.[14] In 2017, O'Hearn and the team open sourced RacerD, an automated static race condition detection tool that reduces the time it takes to flag potential problems in concurrent software, as part of the Infer platform.[22]

O'Hearn was an assistant professor at Syracuse University, New York, United States, from 1990 to 1995. He was a reader in computer science at Queen Mary University of London from 1996 to 1999 and then a full professor at Queen Mary until his move to University College London. At UCL he was granted a Royal Academy of Engineering/Microsoft Research Chair.[23] In 1997 he was a visiting scientist at Carnegie Mellon University and in 2006 he was a visiting researcher at Microsoft Research Cambridge.[17]. He now shares his time working as a research scientist at Facebook and a professor at UCL.

Awards and honours

In 2007, O'Hearn was granted a Royal Society Wolfson Research Merit Award.[4] In 2011, O'Hearn and Samin Ishtiaq were awarded a Most Influential POPL Paper Award.[8] With Stephen Brookes, Carnegie Mellon University, he was co-recipient of the 2016 Gödel Prize, for the invention of Concurrent Separation Logic.[5] Also in 2016, he was elected Fellow of the Royal Academy of Engineering (FREng) and co-received the annual CAV (Computer Aided Verification) award.[6][7] In 2018, he was elected Fellow of the Royal Society (FRS), and was bestowed with an Honorary Doctor of Laws from Dalhousie University.[3][4][2]. January 2019 saw O'Hearn honoured with another Most Influential POPL Paper Award, which he shared with three colleagues.[1]

References

  1. ^ a b "POPL 2019 Most Influential Paper Award for research that led to Facebook Infer". Facebook. 17 January 2019.
  2. ^ a b https://www.dal.ca/news/2018/04/19/introducing-dal-s-honorary-degree-recipients-for-spring-convocat.html
  3. ^ a b "Distinguished scientists elected as Fellows and Foreign Members of the Royal Society". royalsociety.org. Retrieved 15 May 2018.
  4. ^ a b c d e Anon (2018). "Professor Peter O'Hearn FRS". royalsociety.org. London: Royal Society. Archived from the original on 7 June 2018. One or more of the preceding sentences incorporates text from the royalsociety.org website where:

    “All text published under the heading 'Biography' on Fellow profile pages is available under Creative Commons Attribution 4.0 International License.” --"Archived copy". Archived from the original on 11 November 2016. Retrieved 7 June 2018.{{cite web}}: CS1 maint: archived copy as title (link) CS1 maint: bot: original URL status unknown (link)
  5. ^ a b Chita, Efi. "2016 Gödel Prize".
  6. ^ a b c https://www.raeng.org.uk/about-us/the-fellowship/new-fellows-2016/fellows/peter-o-hearn
  7. ^ a b "Four Facebook Employees Win the Prestigious CAV Award". Facebook. 5 September 2016.
  8. ^ a b "Computer Science professor wins prestigious award". Queen Mary University of London. 3 February 2011.
  9. ^ a b c Peter O'Hearn publications indexed by Google Scholar Edit this at Wikidata
  10. ^ a b Peter O'Hearn at the Mathematics Genealogy Project Edit this at Wikidata
  11. ^ Olivier Danvy, Peter O'Hearn and Philip Wadler (editors), Festschrift for John C. Reynolds's 70th Birthday. Theoretical Computer Science, 375(1–3):1–350, 1 May 2007. Editorial, pages 1–2.doi:10.1016/j.tcs.2006.12.024
  12. ^ a b Reynolds, John C. (2002). "Separation Logic: A Logic for Shared Mutable Data Structures" (PDF). LICS.
  13. ^ a b O'Hearn, P. W.; Pym, D. J. (June 1999). "The Logic of Bunched Implications". Bulletin of Symbolic Logic. 5 (2): 215–244. doi:10.2307/421090. JSTOR 421090.
  14. ^ a b c "Infer static analyzer". fbinfer.com.
  15. ^ "Peter O'Hearn". Facebook Research.
  16. ^ "Peter O'Hearn". www0.cs.ucl.ac.uk.
  17. ^ a b Peter W O'Hearn, Curriculum Vitae Archived 2011-07-19 at the Wayback Machine, Queen Mary, University of London, UK.
  18. ^ https://www.facebook.com/academics/videos/2228616734102290/?t=3775
  19. ^ https://dl.acm.org/doi/10.1145/602382.602403
  20. ^ "Facebook Acquires Assets Of UK Mobile Bug-Checking Software Developer Monoidics – TechCrunch". techcrunch.com.
  21. ^ "Continuous Reasoning: Scaling the Impact of Formal Methods". Facebook Research.
  22. ^ "Facebook open sources RacerD: A tool that's already squashed 1,000 bugs in concurrent code". TechRepublic. 19 October 2017.
  23. ^ "Spring Newsletter" (PDF). raeng.org.uk. 2012.

 This article incorporates text available under the CC BY 4.0 license.

Retrieved from "https://en.wikipedia.org/enwiki/w/index.php?title=Peter_O%27Hearn&oldid=933494918"