Peter O'Hearn: Difference between revisions

Peter O'Hearn
FRS FREng
Peter O'Hearn FRS FREng
	O'Hearn in 2018
Born	Peter William O'Hearn; 13 July 1963 (age 61); Halifax, Nova Scotia, Canada
Nationality	British, Canadian
Citizenship	United Kingdom, Canada
Alma mater	Dalhousie University; Queen's University
Known for	Separation logic; Bunched logic; Infer Static Analyzer
Awards	IEEE Cybersecurity Award for Practice (2021); Most Influential POPL Paper Award (2019); Honorary Doctor of Laws, Dalhousie University (2018); Fellow of the Royal Society (FRS) (2018); Gödel Prize (2016); Fellow of the Royal Academy of Engineering (FREng) (2016); CAV (Computer Aided Verification) Award (2016); Most Influential POPL Paper Award (2011); Royal Society Wolfson Research Merit Award (2007);
	Scientific career
Fields	Programming languages; Program analysis; Formal verification; Theoretical computer science
Institutions	Lacework; Meta Platforms; University College London; Queen Mary University of London; Syracuse University
Thesis	Semantics of Non-interference: A natural approach (1992)
Doctoral advisor	Robert D. Tennent
Website	www0.cs.ucl.ac.uk/staff/p.ohearn/

Browse history interactively

← Previous edit

Content deleted Content added

VisualWikitext

Inline

Latest revision as of 14:09, 7 October 2024

Peter William O'Hearn (born 13 July 1963 in Halifax, Nova Scotia), formerly a research scientist at Meta,^[15] is a Distinguished Engineer at Lacework^[16] and a Professor of Computer science at University College London (UCL).^[17] 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.^[10]

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.^[11]^[18]

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 on prior research from O'Hearn and David Pym on logic for resources, termed 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".^[19]

He conducted a study of programming languages which were similar to ALGOL, with his former doctoral advisor Robert D. Tennent, which became the book Algol-Like Languages.^[20]

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 began working at Facebook in 2013 with the acquisition of Monoidics Ltd, a startup he cofounded.^[21] Since its inception, Infer has enabled Facebook engineers to resolve tens of thousands of bugs before reaching production.^[22] 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.^[23]

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 chair sponsored by the Royal Academy of Engineering and Microsoft Research.^[24] In 1997 he was a visiting scientist at Carnegie Mellon University and in 2006 he was a visiting researcher at Microsoft Research Cambridge.^[18] He now shares his time working as a Distinguished Engineer at Lacework and a professor at UCL.^[16]

Awards and honours

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

References

^ ^a ^b "2021 IEEE award ceremony - IEEE Secure Development Conference".
^ ^a ^b "POPL 2019 Most Influential Paper Award for research that led to Facebook Infer". Facebook. 17 January 2019.
^ ^a ^b "Introducing Dal's honorary degree recipients for Spring Convocation 2018".
^ ^a ^b "Distinguished scientists elected as Fellows and Foreign Members of the Royal Society". royalsociety.org. Retrieved 15 May 2018.
^ ^a ^b ^c ^d 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.” --"Terms, conditions and policies | Royal Society". Archived from the original on 11 November 2016. Retrieved 7 June 2018.{{cite web}}: CS1 maint: bot: original URL status unknown (link)
^ ^a ^b Chita, Efi (12–15 July 2016). "2016 Gödel Prize". European Association for Theoretical Computer Science.
^ ^a ^b "Royal Academy Fellows 2016". Archived from the original on 27 March 2019. Retrieved 26 May 2018.
^ ^a ^b O'Sullivan, Bryan (5 September 2016). "Four Facebook Employees Win the Prestigious CAV Award". Facebook.^{[unreliable source?]}
^ ^a ^b "Computer Science professor wins prestigious award". Queen Mary University of London. 3 February 2011.
^ ^a ^b ^c Peter O'Hearn publications indexed by Google Scholar
^ ^a ^b Peter O'Hearn at the Mathematics Genealogy Project
^ ^a ^b Reynolds, John C. (2002). "Separation Logic: A Logic for Shared Mutable Data Structures" (PDF). LICS.
^ ^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. S2CID 2948552.
^ ^a ^b ^c "Infer static analyzer". fbinfer.com.
^ "Peter O'Hearn". Facebook Research.
^ ^a ^b "Peter O'Hearn".
^ "Peter O'Hearn". www0.cs.ucl.ac.uk.
^ ^a ^b Peter W O'Hearn, Curriculum Vitae Archived 19 July 2011 at the Wayback Machine, Queen Mary, University of London, UK.
^ Hoare, Tony (2003). "The verifying compiler". Journal of the ACM. 50: 63–69. doi:10.1145/602382.602403. S2CID 441648.
^ O'Hearn, Peter; Tennent, Robert D. (1997). Algol-Like Languages. Cambridge, MA: Birkhauser Boston. doi:10.1007/978-1-4612-4118-8. ISBN 978-0-8176-3880-1. S2CID 6273486.
^ "Facebook Acquires Assets Of UK Mobile Bug-Checking Software Developer Monoidics". TechCrunch. Verizon Media. 18 July 2013.
^ "Continuous Reasoning: Scaling the Impact of Formal Methods". Facebook Research.
^ "Facebook open sources RacerD: A tool that's already squashed 1,000 bugs in concurrent code". TechRepublic. 19 October 2017.
^ "Spring Newsletter". raeng.org.uk. 2012. Archived from the original on 4 September 2016. Retrieved 6 June 2018.

External links

Media related to Peter O'Hearn at Wikimedia Commons

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

[secdev.ieee.org-1] "2021 IEEE award ceremony - IEEE Secure Development Conference".

[poplaward2-2] "POPL 2019 Most Influential Paper Award for research that led to Facebook Infer". Facebook. 17 January 2019.

[dal.ca-3] "Introducing Dal's honorary degree recipients for Spring Convocation 2018".

[royalsociety.org-4] "Distinguished scientists elected as Fellows and Foreign Members of the Royal Society". royalsociety.org. Retrieved 15 May 2018.

[frs-5] 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.” --"Terms, conditions and policies | Royal Society". Archived from the original on 11 November 2016. Retrieved 7 June 2018.{{cite web}}: CS1 maint: bot: original URL status unknown (link)

[auto-6] Chita, Efi (12–15 July 2016). "2016 Gödel Prize". European Association for Theoretical Computer Science.

[raeng.org.uk-7] "Royal Academy Fellows 2016". Archived from the original on 27 March 2019. Retrieved 26 May 2018.

[fbcav-8] O'Sullivan, Bryan (5 September 2016). "Four Facebook Employees Win the Prestigious CAV Award". Facebook.^{[unreliable source?]}

[poplaward-9] "Computer Science professor wins prestigious award". Queen Mary University of London. 3 February 2011.

[gs-10] Peter O'Hearn publications indexed by Google Scholar

[mathgene-11] Peter O'Hearn at the Mathematics Genealogy Project

[lics02-12] Reynolds, John C. (2002). "Separation Logic: A Logic for Shared Mutable Data Structures" (PDF). LICS.

[bi-13] 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. S2CID 2948552.

[fbinfer-14] "Infer static analyzer". fbinfer.com.

[15] "Peter O'Hearn". Facebook Research.

[www0.cs.ucl.ac.uk-16] "Peter O'Hearn".

[17] "Peter O'Hearn". www0.cs.ucl.ac.uk.

[cv-18] Peter W O'Hearn, Curriculum Vitae Archived 19 July 2011 at the Wayback Machine, Queen Mary, University of London, UK.

[19] Hoare, Tony (2003). "The verifying compiler". Journal of the ACM. 50: 63–69. doi:10.1145/602382.602403. S2CID 441648.

[20] O'Hearn, Peter; Tennent, Robert D. (1997). Algol-Like Languages. Cambridge, MA: Birkhauser Boston. doi:10.1007/978-1-4612-4118-8. ISBN 978-0-8176-3880-1. S2CID 6273486.

[21] "Facebook Acquires Assets Of UK Mobile Bug-Checking Software Developer Monoidics". TechCrunch. Verizon Media. 18 July 2013.

[22] "Continuous Reasoning: Scaling the Impact of Formal Methods". Facebook Research.

[23] "Facebook open sources RacerD: A tool that's already squashed 1,000 bugs in concurrent code". TechRepublic. 19 October 2017.

[24] "Spring Newsletter". raeng.org.uk. 2012. Archived from the original on 4 September 2016. Retrieved 6 June 2018.

[12]

[13]

[14]

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

[22]

[23]

[24]

@@ Line 1: / Line 1: @@
-{{Short description|Research scientist}}
+{{Short description|Research scientist (born 1963)}}
 {{Use Canadian English|date=April 2018}}
 {{Use dmy dates|date=April 2018}}
 {{Infobox scientist
-| name = Peter O'Hearn
+| name              = Peter O'Hearn
-| image = Peter O'Hearn Royal Society.jpg
+| image             = Peter O'Hearn Royal Society.jpg
-| honorific_suffix = {{post-nominals|country=GBR|FRS|FREng|size=100%}}
+| honorific_suffix  = {{post-nominals|country=GBR|FRS|FREng|size=100%}}
-| caption = Peter O'Hearn at the [[Royal Society]] admissions day in London, July 2018
+| caption           = O'Hearn in 2018
-| birth_date = {{Birth date and age|df=yes|1963|7|13}}
+| birth_date        = {{Birth date and age|df=yes|1963|7|13}}
-| birth_name = Peter William O'Hearn
+| birth_name        = Peter William O'Hearn
-| birth_place = [[Halifax, Nova Scotia]], Canada
+| birth_place       = [[Halifax, Nova Scotia]], Canada
-| citizenship = United Kingdom, Canada
+| citizenship       = United Kingdom, Canada
-| nationality = British, Canadian
+| nationality       = British, Canadian
-| ethnicity =
+| ethnicity         =
-| fields = [[Programming language]]s<ref name=gs/><br />[[Program analysis]]<br />[[Formal verification]]<br />[[Theoretical computer science]]<ref name=gs/>
+| fields            = [[Programming language]]s<ref name=gs/><br />[[Program analysis]]<br />[[Formal verification]]<br />[[Theoretical computer science]]<ref name=gs/>
-| workplaces = Lacework<br />[[Meta Platforms]]<br />[[University College London]]<br />[[Queen Mary University of London]]<br />[[Syracuse University]]
+| workplaces        = Lacework<br />[[Meta Platforms]]<br />[[University College London]]<br />[[Queen Mary University of London]]<br />[[Syracuse University]]
-| alma_mater = [[Dalhousie University]] (BSc)<br />[[Queen's University at Kingston|Queen's University]] (MSc, PhD)
+| alma_mater        = [[Dalhousie University]]<br />[[Queen's University at Kingston|Queen's University]]
-| doctoral_advisor = Robert D. Tennent<ref name=mathgene>{{MathGenealogy}}</ref>
+| doctoral_advisor  = Robert D. Tennent<ref name=mathgene>{{MathGenealogy}}</ref>
-| thesis_title = Semantics of Non-interference: A natural approach
+| thesis_title      = Semantics of Non-interference: A natural approach
-| thesis_url = https://dl.acm.org/citation.cfm?id=143966
+| thesis_url        = https://dl.acm.org/citation.cfm?id=143966
-| thesis_year = 1992
+| thesis_year       = 1992
 | academic_advisors =
 | doctoral_students =
-| notable_students =
+| notable_students  =
-| 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 |author-link=John C. Reynolds |journal=LICS |year=2002}}</ref><br />[[Bunched logic]]<ref name="bi">{{cite journal |title=The Logic of Bunched Implications |first1=P. W. |last1=O'Hearn |first2=D. J. |last2=Pym |date=June 1999 |journal=[[Bulletin of Symbolic Logic]] |volume=5 |number=2 |pages=215–244 |doi=10.2307/421090 |jstor=421090 |s2cid=2948552 |url=https://semanticscholar.org/paper/99ee6eb28490ffce90716365c4e0a3b1018738eb}}</ref><br />[[Infer Static Analyzer]]<ref name=fbinfer>{{cite web |url=http://fbinfer.com/ |title=Infer static analyzer |website=fbinfer.com}}</ref>
+| 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 |author-link=John C. Reynolds |journal=LICS |year=2002}}</ref><br />[[Bunched logic]]<ref name="bi">{{cite journal |title=The Logic of Bunched Implications |first1=P. W. |last1=O'Hearn |first2=D. J. |last2=Pym |date=June 1999 |journal=[[Bulletin of Symbolic Logic]] |volume=5 |number=2 |pages=215–244 |doi=10.2307/421090 |jstor=421090 |s2cid=2948552 }}</ref><br />[[Infer Static Analyzer]]<ref name=fbinfer>{{cite web |url=http://fbinfer.com/ |title=Infer static analyzer |website=fbinfer.com}}</ref>
+| awards            = {{Plainlist|<!-- significant awards, e.g. those with dedicated wikipedia articles-->
-| influences = [[John C. Reynolds]]<ref>Olivier Danvy, Peter O'Hearn and [[Philip Wadler]] (editors), Festschrift for John C. Reynolds's 70th Birthday. ''[[Theoretical Computer Science (journal)|Theoretical Computer Science]]'', 375(1–3):1–350, 1 May 2007. Editorial, pages 1–2.{{doi|10.1016/j.tcs.2006.12.024}}</ref>
-| influenced =
-| awards = {{Plainlist|<!-- significant awards, e.g. those with dedicated wikipedia articles-->
 *IEEE Cybersecurity Award for Practice (2021)<ref name="secdev.ieee.org">{{Cite web|url=https://secdev.ieee.org/2021/ieee-award-ceremony/|title = 2021 IEEE award ceremony - IEEE Secure Development Conference}}</ref>
 *Most Influential POPL Paper Award (2019)<ref name="poplaward2">{{cite web |url=https://research.fb.com/blog/2019/01/popl-2019-most-influential-paper-award-for-research-that-led-to-facebook-infer/ |title= POPL 2019 Most Influential Paper Award for research that led to Facebook Infer |date=17 January 2019 |publisher=[[Facebook]]}}</ref>
 *Honorary [[Doctor of Laws]], [[Dalhousie University]] (2018)<ref name="dal.ca">{{Cite web|url=https://www.dal.ca/news/2018/04/19/introducing-dal-s-honorary-degree-recipients-for-spring-convocat.html|title = Introducing Dal's honorary degree recipients for Spring Convocation 2018}}</ref>
-*[[Fellow of the Royal Society]] (FRS) (2018)<ref name="royalsociety.org">{{cite web |url=https://royalsociety.org/news/2018/05/distinguished-scientists-elected-fellows-royal-society-2018/ |title=Distinguished scientists elected as Fellows and Foreign Members of the Royal Society |website=royalsociety.org |language=en-gb |access-date=2018-05-15}}</ref><ref name=frs/>
+*[[Fellow of the Royal Society]] (FRS) (2018)<ref name="royalsociety.org">{{cite web |url=https://royalsociety.org/news/2018/05/distinguished-scientists-elected-fellows-royal-society-2018/ |title=Distinguished scientists elected as Fellows and Foreign Members of the Royal Society |website=royalsociety.org |df=dmy-all|access-date=2018-05-15}}</ref><ref name=frs>{{cite web |url=https://royalsociety.org/people/peterohearn13830/ |website=royalsociety.org |title=Professor Peter O'Hearn FRS |publisher=[[Royal Society]]|location=London|author=Anon|year=2018|archive-url=https://web.archive.org/web/20180607074505/https://royalsociety.org/people/peterohearn13830/|archivedate=7 June 2018}} One or more of the preceding sentences incorporates text from the royalsociety.org website where: {{blockquote|“All text published under the heading 'Biography' on Fellow profile pages is available under [[Creative Commons license|Creative Commons Attribution 4.0 International License]].” --{{Cite web |url=https://royalsociety.org/about-us/terms-conditions-policies/ |title=Terms, conditions and policies &#124; Royal Society |access-date=7 June 2018 |archive-url=https://web.archive.org/web/20161111170346/https://royalsociety.org/about-us/terms-conditions-policies/ |archive-date=11 November 2016 |url-status=bot: unknown |df=dmy-all}}}}</ref>
 *[[Gödel Prize]] (2016)<ref name="auto">{{cite web |first=Efi |last=Chita |date=12–15 July 2016 |url=https://eatcs.org/index.php/component/content/article/1-news/2280-2016-godel-prize |title=2016 Gödel Prize |publisher=European Association for Theoretical Computer Science}}</ref>
-* [[Fellow of the Royal Academy of Engineering]] (FREng) (2016)<ref name="raeng.org.uk">https://www.raeng.org.uk/about-us/the-fellowship/new-fellows-2016/fellows/peter-o-hearn</ref>
+* [[Fellow of the Royal Academy of Engineering]] (FREng) (2016)<ref name="raeng.org.uk">{{Cite web |url=https://www.raeng.org.uk/about-us/the-fellowship/new-fellows-2016/fellows/peter-o-hearn |title=Royal Academy Fellows 2016 |access-date=26 May 2018 |archive-date=27 March 2019 |archive-url=https://web.archive.org/web/20190327124215/https://www.raeng.org.uk/about-us/the-fellowship/new-fellows-2016/fellows/peter-o-hearn |url-status=dead }}</ref>
-*CAV (Computer Aided Verification) Award (2016)<ref name="fbcav">{{cite web |last=O'Sullivan |first=Bryan |date=5 September 2016 |url=https://research.fb.com/blog/2016/09/four-facebook-employees-win-the-prestigious-cav-award/ |title=Four Facebook Employees Win the Prestigious CAV Award |publisher=[[Facebook]]}}</ref>
+*CAV (Computer Aided Verification) Award (2016)<ref name="fbcav">{{cite web |last=O'Sullivan |first=Bryan |date=5 September 2016 |url=https://research.fb.com/blog/2016/09/four-facebook-employees-win-the-prestigious-cav-award/ |title=Four Facebook Employees Win the Prestigious CAV Award |publisher=[[Facebook]]}}{{unreliable source?|date=November 2022}}</ref>
 *Most Influential POPL Paper Award (2011)<ref name="poplaward">{{cite web |url=https://www.qmul.ac.uk/media/news/2011/se/computer-science-professor-wins-prestigious-award.html |title=Computer Science professor wins prestigious award |date=3 February 2011 |publisher=[[Queen Mary University of London]]}}</ref>
 * [[Royal Society Wolfson Research Merit Award]] (2007)<ref name=frs/>}}
-| website = {{URL|http://www0.cs.ucl.ac.uk/staff/p.ohearn/}}
+| website           = {{URL|http://www0.cs.ucl.ac.uk/staff/p.ohearn/}}
 }}
+'''Peter William O'Hearn''' (born 13 July 1963 in [[Halifax, Nova Scotia]]), formerly a research scientist at [[Meta Platforms|Meta]],<ref>{{cite web |url=https://research.fb.com/people/ohearn-peter/ |title=Peter O'Hearn |website=Facebook Research}}</ref> is a Distinguished Engineer at Lacework<ref name="www0.cs.ucl.ac.uk">{{Cite web|url=http://www0.cs.ucl.ac.uk/staff/p.ohearn/|title = Peter O'Hearn}}</ref> and a [[Professor]] of [[Computer science]] at [[University College London]] (UCL).<ref>{{cite web |url=http://www0.cs.ucl.ac.uk/staff/p.ohearn/ |title=Peter O'Hearn |website=www0.cs.ucl.ac.uk}}</ref> 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.<ref name=gs>{{Google Scholar id}}</ref>
-'''Peter William O'Hearn''' {{post-nominals|country=GBR|FRS|FREng}}<ref name=frs>{{cite web |url=https://royalsociety.org/people/peterohearn13830/ |website=royalsociety.org |title=Professor Peter O'Hearn FRS |publisher=[[Royal Society]]|location=London|author=Anon|year=2018|archiveurl=https://web.archive.org/web/20180607074505/https://royalsociety.org/people/peterohearn13830/|archivedate=2018-06-07}} One or more of the preceding sentences incorporates text from the royalsociety.org website where: {{blockquote|“All text published under the heading 'Biography' on Fellow profile pages is available under [[Creative Commons license|Creative Commons Attribution 4.0 International License]].” --{{Cite web |url=https://royalsociety.org/about-us/terms-conditions-policies/ |title=Terms, conditions and policies &#124; Royal Society |access-date=7 June 2018 |archive-url=https://web.archive.org/web/20161111170346/https://royalsociety.org/about-us/terms-conditions-policies/# |archive-date=11 November 2016 |url-status=bot: unknown |df=dmy-all}}}}</ref><ref name="raeng.org.uk">https://www.raeng.org.uk/about-us/the-fellowship/new-fellows-2016/fellows/peter-o-hearn</ref> (born 13 July 1963 in [[Halifax, Nova Scotia]]), formerly a research scientist at [[Meta Platforms|Meta]],<ref>{{cite web |url=https://research.fb.com/people/ohearn-peter/ |title=Peter O'Hearn |website=Facebook Research}}</ref> is a Distinguished Engineer at Lacework<ref name="www0.cs.ucl.ac.uk">{{Cite web|url=http://www0.cs.ucl.ac.uk/staff/p.ohearn/|title = Peter O'Hearn}}</ref> and a [[Professor]] of [[Computer science]] at [[University College London]] (UCL).<ref>{{cite web |url=http://www0.cs.ucl.ac.uk/staff/p.ohearn/ |title=Peter O'Hearn |website=www0.cs.ucl.ac.uk}}</ref> 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.<ref name=gs>{{Google Scholar id}}</ref>
 ==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 at Kingston|Queen's University]], [[Kingston, Ontario|Kingston]], [[Ontario]], Canada. His dissertation was on ''Semantics of Non-interference: A natural approach'', supervised by Robert D. Tennent.<ref name=mathgene/><ref name="cv">[http://www.eecs.qmul.ac.uk/~ohearn/CV.pdf Peter W O'Hearn, Curriculum Vitae] {{webarchive |url=https://web.archive.org/web/20110719174954/http://www.eecs.qmul.ac.uk/~ohearn/CV.pdf |date=2011-07-19}}, [[Queen Mary, University of London]], UK.</ref>
+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 at Kingston|Queen's University]], [[Kingston, Ontario|Kingston]], [[Ontario]], Canada. His dissertation was on ''Semantics of Non-interference: A natural approach'', supervised by Robert D. Tennent.<ref name=mathgene/><ref name="cv">[http://www.eecs.qmul.ac.uk/~ohearn/CV.pdf Peter W O'Hearn, Curriculum Vitae] {{webarchive |url=https://web.archive.org/web/20110719174954/http://www.eecs.qmul.ac.uk/~ohearn/CV.pdf |date=19 July 2011}}, [[Queen Mary, University of London]], UK.</ref>
 ==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 |author-link=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 on prior research from O'Hearn and David Pym on logic for resources, termed [[bunched logic]].<ref name="bi" /> 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 {{User-generated source|certain=yes|date=March 2022}}</ref><ref>{{Cite journal|url=https://dl.acm.org/doi/10.1145/602382.602403|doi = 10.1145/602382.602403|title = The verifying compiler|year = 2003|last1 = Hoare|first1 = Tony|journal = Journal of the ACM|volume = 50|pages = 63–69|s2cid = 441648}}</ref>
+O'Hearn is best known for [[separation logic]],<ref name="lics02"/> a theory he developed with [[John C. Reynolds]] that unearthed new domains for scaling logical reasoning about code. This built on prior research from O'Hearn and David Pym on logic for resources, termed [[bunched logic]].<ref name="bi" /> 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>{{Cite journal|url=https://dl.acm.org/doi/10.1145/602382.602403|doi = 10.1145/602382.602403|title = The verifying compiler|year = 2003|last1 = Hoare|first1 = Tony|journal = Journal of the ACM|volume = 50|pages = 63–69|s2cid = 441648}}</ref>
-He conducted a study of programming languages which were similar to [[ALGOL]], with his former doctoral advisor Robert D. Tennent, which became the book ''Algol-Like Languages''.<ref>{{cite book |last1=O'Hearn |first1=Peter |last2=Tennent |first2=Robert D. |date=1997 |title=Algol-Like Languages |publisher=Birkhauser Boston |place=Cambridge, Massachusetts, United States |isbn=978-0-8176-3880-1 |doi=10.1007/978-1-4612-4118-8|s2cid=6273486 }}</ref>
+He conducted a study of programming languages which were similar to [[ALGOL]], with his former doctoral advisor Robert D. Tennent, which became the book ''Algol-Like Languages''.<ref>{{cite book |last1=O'Hearn |first1=Peter |last2=Tennent |first2=Robert D. |year=1997 |title=Algol-Like Languages |publisher=Birkhauser Boston |place=Cambridge, MA|isbn=978-0-8176-3880-1 |doi=10.1007/978-1-4612-4118-8|s2cid=6273486 }}</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 began working 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 |website=TechCrunch |publisher=Verizon Media}}</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 began working 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 |website=TechCrunch |date=18 July 2013 |publisher=Verizon Media}}</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>
 O'Hearn was an assistant professor at [[Syracuse University]], [[New York (state)|New York]], United States, from 1990 to 1995.
-He was a [[Reader (academic rank)|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 Chair sponsored by the [[Royal Academy of Engineering]] and [[Microsoft Research]].<ref>{{cite web |url=https://www.raeng.org.uk/publications/newsletters/spring-newsletter-2012 |title=Spring Newsletter |date=2012 |website=raeng.org.uk |format=PDF}}</ref> In 1997 he was a visiting scientist at [[Carnegie Mellon University]] and in 2006 he was a visiting researcher at [[Microsoft Research Cambridge]].<ref name="cv" /> He now shares his time working as a Distinguished Engineer at Lacework and a professor at UCL.<ref name="www0.cs.ucl.ac.uk"/>
+He was a [[Reader (academic rank)|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 chair sponsored by the [[Royal Academy of Engineering]] and [[Microsoft Research]].<ref>{{cite web |url=https://www.raeng.org.uk/publications/newsletters/spring-newsletter-2012 |title=Spring Newsletter |year=2012 |website=raeng.org.uk |access-date=6 June 2018 |archive-date=4 September 2016 |archive-url=https://web.archive.org/web/20160904160433/http://www.raeng.org.uk/publications/newsletters/spring-newsletter-2012 |url-status=dead }}</ref> In 1997 he was a visiting scientist at [[Carnegie Mellon University]] and in 2006 he was a visiting researcher at [[Microsoft Research Cambridge]].<ref name="cv" /> He now shares his time working as a Distinguished Engineer at Lacework and a professor at UCL.<ref name="www0.cs.ucl.ac.uk"/>
 ===Awards and honours===
-In 2007, O'Hearn was granted a [[Royal Society Wolfson Research Merit Award]].<ref name=frs/> In 2011, O'Hearn and Samin Ishtiaq were awarded a Most Influential POPL Paper Award.<ref name="poplaward" /> With Stephen Brookes, [[Carnegie Mellon University]], he was co-recipient of the 2016 [[Gödel Prize]], for the invention of Concurrent Separation Logic.<ref name="auto"/> Also in 2016, he was elected [[Fellow of the Royal Academy of Engineering]] (FREng) and co-received the annual CAV (Computer Aided Verification) award.<ref name="raeng.org.uk">https://www.raeng.org.uk/about-us/the-fellowship/new-fellows-2016/fellows/peter-o-hearn</ref><ref name="fbcav" /> In 2018, he was elected [[Fellow of the Royal Society]] (FRS), and was bestowed with an Honorary [[Doctor of Laws]] from [[Dalhousie University]].<ref name="royalsociety.org">{{cite web |url=https://royalsociety.org/news/2018/05/distinguished-scientists-elected-fellows-royal-society-2018/ |title=Distinguished scientists elected as Fellows and Foreign Members of the Royal Society |website=royalsociety.org |language=en-gb |access-date=2018-05-15}}</ref><ref name=frs/><ref name="dal.ca">{{Cite web|url=https://www.dal.ca/news/2018/04/19/introducing-dal-s-honorary-degree-recipients-for-spring-convocat.html|title = Introducing Dal's honorary degree recipients for Spring Convocation 2018}}</ref> January 2019 saw O'Hearn honoured with another Most Influential POPL Paper Award, which he shared with three colleagues.<ref name="poplaward2" /> The [[Institute of Electrical and Electronics Engineers (IEEE)]] granted O'Hearn and three of his Facebook colleagues an IEEE Cybersecurity Award for Practice at their annual awards ceremony in October, 2021.<ref name="secdev.ieee.org">{{Cite web|url=https://secdev.ieee.org/2021/ieee-award-ceremony/|title = 2021 IEEE award ceremony - IEEE Secure Development Conference}}</ref>
+In 2007, O'Hearn was granted a [[Royal Society Wolfson Research Merit Award]].<ref name=frs/> In 2011, O'Hearn and Samin Ishtiaq were awarded a Most Influential POPL Paper Award.<ref name="poplaward" /> With Stephen Brookes, [[Carnegie Mellon University]], he was co-recipient of the 2016 [[Gödel Prize]], for the invention of Concurrent Separation Logic.<ref name="auto"/> Also in 2016, he was elected [[Fellow of the Royal Academy of Engineering]] (FREng) and co-received the annual CAV (Computer Aided Verification) award.<ref name="raeng.org.uk"/><ref name="fbcav" /> In 2018, he was elected [[Fellow of the Royal Society]] (FRS), and was bestowed with an Honorary [[Doctor of Laws]] from [[Dalhousie University]].<ref name="royalsociety.org"/><ref name=frs/><ref name="dal.ca"/> January 2019 saw O'Hearn honoured with another Most Influential POPL Paper Award, which he shared with three colleagues.<ref name="poplaward2" /> The [[Institute of Electrical and Electronics Engineers (IEEE)]] granted O'Hearn and three of his Facebook colleagues an IEEE Cybersecurity Award for Practice at their annual awards ceremony in October, 2021.<ref name="secdev.ieee.org"/>
-== References ==
+==References==
 {{Reflist}}
+==External links==
+*{{Commons-inline}}
 {{CC-notice |cc=by4 |url=https://royalsociety.org/people/peterohearn13830/}}
@@ Line 75: / Line 74: @@
 [[Category:Canadian computer scientists]]
 [[Category:Formal methods people]]
-[[Category:Fellows of the Royal Society]]
+[[Category:Canadian fellows of the Royal Society]]
 [[Category:Fellows of the Royal Academy of Engineering]]
 [[Category:Syracuse University faculty]]

v t e Fellows of the Royal Society elected in 2018
Fellows	Jim Al-Khalili Polly Arnold Jillian Banfield Margaret Brimble Neil Brockdorff Frank Caruso Vincenzo Cerundolo Kevin Costello Robert Crabtree Philip Dawid Peter Dayan Richard Dixon Gregory Edgecombe Wenfei Fan Roger Goody Robin Grimes Gregory Hannon Demis Hassabis Judy Hirst Graeme Jameson Harren Jhoti Sophien Kamoun Andrew King Dimitri Kullmann Dominic Kwiatkowski Richard Marais Cathie Martin Elon Musk Peter O'Hearn Vassilis Pachnis Tracy Palmer Colin Prentice Lalita Ramakrishnan Nancy Reid Graham Richards David Richardson Sheila Rowan Ingrid Scheffer Michelle Simmons John Smol Timothy Softley John Speakman Graeme Stephens Angela Strank Charles Swanton Peter Visscher Guy Wilkinson Geordie Williamson Daniel Wise Nikolay Zheludev
Honorary	David Willetts (Baron Willetts of Havant)
Foreign	Carolyn Bertozzi Martin Chalfie Sebsebe Demissew Jeffrey Friedman Fabiola Gianotti Albrecht Hofmann Butler Lampson Tullio Pozzan Joachim Sauer Adi Shamir

Authority control databases
International	ISNI VIAF WorldCat
National	Germany United States France BnF data Netherlands
Academics	ORCID Mathematics Genealogy Project Association for Computing Machinery Google Scholar DBLP MathSciNet
Other	IdRef