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.
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 Foreword by Mike Mislove and Prakash Panangaden
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