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:
- RacerD: Compositional Static Race Detection. OOPSLA'18
-
Experience developing and deploying concurrency analysis at Facebook
Paper to go with my 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. -
Open-sourcing RacerD: Fast static race detection at scale.
Facebook Engineering Blog Post -
Finding Interprocedural Bugs at Scale with Infer Static Analyzer
Facebook Engineering Blog Post -
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