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.
- A True Positives Theorem for a Static Race Detector POPL'19
- RacerD: Compositional Static Race Detection. OOPSLA'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 to go with my plenary talk at the FLOC conferences in July.
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.
- From Categorical Logic to Facebook Engineering. LICS 2015: 17-21
- Moving Fast with Software Verification. NASA Formal Methods symposium 2015: 3-11
- The Essence of Reynolds. Tribute to John C. Reynolds. POPL'14, pages 251-255. Also published in Formal Asp. Comput. 26(3): 435-439 (2014)
- A Primer on Separation Logic (and Automatic Program Verification and Analysis).
- Tutorial on Separation Logic. (slides)
email: p.ohearn AT ucl.ac.uk