| 词条 | Peter O'Hearn |
| 释义 |
| name = Peter O'Hearn | image = Peter O'Hearn Royal Society.jpg | honorific_suffix = {{post-nominals|country=GBR|FRS|FREng|size=100%}} | image_size = | caption = Peter O'Hearn at the Royal Society admissions day in London, July 2018 | birth_date = {{b-da|13 July 1963}} | birth_name = Peter William O'Hearn | birth_place = Halifax, Nova Scotia, Canada | death_date = | death_place = | residence = | citizenship = United Kingdom/Canada | nationality = British/Canadian | ethnicity = | fields = Programming languages[1] Program analysis Formal verification Theoretical computer science[1] | workplaces = Facebook University College London Queen Mary University of London Syracuse University | alma_mater = Dalhousie University (BSc) Queen's University (MSc, PhD) | doctoral_advisor = Robert D. Tennent[1] | thesis_title = Semantics of Non-interference: A natural approach | thesis_url = https://dl.acm.org/citation.cfm?id=143966 | thesis_year = 1992 | academic_advisors = | doctoral_students = | notable_students = | known_for = Separation logic[2] Bunched logic[3] Infer Static Analyzer[4] | influences = John C. Reynolds[5] | influenced = | awards = {{Plainlist|
| website = {{URL|http://www0.cs.ucl.ac.uk/staff/p.ohearn/}} }}Peter William O'Hearn {{post-nominals|country=GBR|FRS|FREng}}[13][14] (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.[17] EducationO'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.[1][18] Career and researchO'Hearn is best known for separation logic,[19] 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.[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.[4] After 20 plus years in academia, O'Hearn landed 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.[4] 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.[18]. He now shares his time working as a research scientist at Facebook and a professor at UCL. Awards and honoursIn 2007, O'Hearn was granted a Royal Society Wolfson Research Merit Award.[13] In 2011, O'Hearn and Samin Ishtiaq were awarded a Most Influential POPL Paper Award.[24] With Stephen Brookes, Carnegie Mellon University, he was co-recipient of the 2016 Gödel Prize, for the invention of Concurrent Separation Logic.[9] Also in 2016, he was elected Fellow of the Royal Academy of Engineering (FREng) and co-received the annual CAV (Computer Aided Verification) award.[25][26] In 2018, he was elected Fellow of the Royal Society (FRS), and was bestowed with an Honorary Doctor of Laws from Dalhousie University.[27][13][28]. January 2019 saw O'Hearn honoured with another Most Influential POPL Paper Award, which he shared with three colleagues.[29] References1. ^1 {{MathGenealogy}} {{CC-notice|cc=by4|url= https://royalsociety.org/people/peterohearn13830/}}{{FRS 2018}}{{Authority control}}{{DEFAULTSORT:Ohearn, Peter}}2. ^{{cite journal| url=http://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 | work=LICS | year=2002 }} 3. ^{{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 }} 4. ^1 2 {{cite web|url=http://fbinfer.com/|title=Infer static analyzer|website=fbinfer.com}} 5. ^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}} 6. ^https://www.qmul.ac.uk/media/news/2011/se/computer-science-professor-wins-prestigious-award.html 7. ^https://www.dal.ca/news/2018/04/19/introducing-dal-s-honorary-degree-recipients-for-spring-convocat.html 8. ^{{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}} 9. ^1 {{cite web|url=http://eatcs.org/index.php/component/content/article/1-news/2280-2016-godel-prize,|title=2016 Gödel Prize|first=Efi|last=Chita|publisher=}} 10. ^https://www.raeng.org.uk/about-us/the-fellowship/new-fellows-2016/fellows/peter-o-hearn 11. ^https://research.fb.com/four-facebook-employees-win-the-prestigious-cav-award/ 12. ^https://www.qmul.ac.uk/media/news/2011/se/computer-science-professor-wins-prestigious-award.html 13. ^1 2 3 4 {{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: {{quote|“All text published under the heading 'Biography' on Fellow profile pages is available under Creative Commons Attribution 4.0 International License.” --{{Cite web |url=https://royalsociety.org/about-us/terms-conditions-policies/ |title=Archived copy |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 |dead-url=bot: unknown |df=dmy-all }}}} 14. ^https://www.raeng.org.uk/about-us/the-fellowship/new-fellows-2016/fellows/peter-o-hearn 15. ^{{cite web|url=https://research.fb.com/people/ohearn-peter/|title=Peter O’Hearn|website=Facebook Research}} 16. ^{{cite web|url=http://www0.cs.ucl.ac.uk/staff/p.ohearn/|title=Peter O'Hearn|website=www0.cs.ucl.ac.uk}} 17. ^1 2 {{Google scholar id}} 18. ^1 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. 19. ^{{cite journal| url=http://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 | work=LICS | year=2002 }} 20. ^{{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 }} 21. ^{{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}} 22. ^{{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}} 23. ^{{cite web|url=https://www.raeng.org.uk/publications/newsletters/spring-newsletter-2012 |title=Spring Newsletter |date=2012 |website=raeng.org.uk |format=PDF}} 24. ^https://www.qmul.ac.uk/media/news/2011/se/computer-science-professor-wins-prestigious-award.html 25. ^https://www.raeng.org.uk/about-us/the-fellowship/new-fellows-2016/fellows/peter-o-hearn 26. ^https://research.fb.com/four-facebook-employees-win-the-prestigious-cav-award/ 27. ^{{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}} 28. ^https://www.dal.ca/news/2018/04/19/introducing-dal-s-honorary-degree-recipients-for-spring-convocat.html 29. ^https://www.qmul.ac.uk/media/news/2011/se/computer-science-professor-wins-prestigious-award.html 17 : 1963 births|Living people|People from Halifax, Nova Scotia|Dalhousie University alumni|Queen's University alumni|Canadian emigrants to England|British computer scientists|Canadian computer scientists|Formal methods people|Fellows of the Royal Society|Fellows of the Royal Academy of Engineering|Syracuse University faculty|Academics of Queen Mary University of London|Academics of University College London|Facebook employees|Gödel Prize laureates|Royal Society Wolfson Research Merit Award holders |
| 随便看 |
|
开放百科全书收录14589846条英语、德语、日语等多语种百科知识，基本涵盖了大多数领域的百科知识，是一部内容自由、开放的电子版国际百科全书。