I am a Professor of Computer Science at University College London and a Research scientist at Facebook. My research has stretched from abstract topics such as category-theoretic models and logics through to logics of programs and on to automated analysis of industrial software in the million of lines of code and its deployment to products used regularly by billions of people. I like to think that fundamental theory, tool development and application can and even should play off one another via mutual feedback in computer science research, in a way reminiscent of the experimental method.
Recent:
- Formal Reasoning and the Hacker Way. ICSE'20 keynote. Video of talk
- Incorrectness Logic. POPL'20. errata (typos). Video of talk
- Scaling Static Analyses at Facebook. Communications of the ACM, Volume 62 Issue 8, August 2019, Pages 62-70.
- Separation Logic. Communications of the ACM, February 2019, Vol. 62 No. 2, Pages 86-95. ( Appendix on Mechanized Reasoning )
- POPL 2019 Most Influential Paper Award for research that led to Facebook Infer
- A True Positives Theorem for a Static Race Detector POPL'19
- RacerD: Compositional Static Race Detection. OOPSLA'18
- From Start-ups to Scale-ups: Opportunities and Open Problems for Static and Dynamic Program Analysis. M Harman and P O'Hearn. Invited paper at SCAM'18
- Experience developing and deploying concurrency analysis at Facebook. Invited tutorial at SAS'18
- Continuous Reasoning: Scaling the impact of formal methods. LICS'18.
-
Concurrent Separation Logic.
Steve Brookes and Peter O'Hearn. ACM SIGLOG News Vol 3, No 3, pp 47-65, July 2016 - The essence of Reynolds, paper+talk
-
CurryOn'16 talk on deploying
Infer at Facebook.
email: p.ohearn AT ucl.ac.uk