I am a Professor of Computer Science at University College London. I'm also an Engineering Director at Facebook, where I work on developing and deploying techniques from program verification and static analysis.
My research has been in the areas of programming languages and logic. I have worked on theoretical topics (e.g., on new logics and category-theoretic models...) and on practical tools for program verification and analysis (e.g., Smallfoot, Space Invader, Abductor, Infer). 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.
- CSL retrospective paper
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