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.
- 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 paper associated with my plenary talk at FLoc
- Why Separation Logic Works D Pym, JM Spring, and P O'Hearn. P. Philos. Technol. (2018)
Concurrent Separation Logic.
Steve Brookes and Peter O'Hearn. ACM SIGLOG News Vol 3, No 3, pp 47-65, July 2016
CurryOn'16 talk on deploying
Infer at Facebook.
Moving Fast with Software Verification.
NASA Formal Methods symposium 2015: 3-11
email: p.ohearn AT ucl.ac.uk