I am a Professor of Computer Science at University College London. I'm also an Engineering Manager at Facebook, where I work with the Static Analysis Tools team out of the London Engineering office.
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.
- Slides from CAV'15 invited talk on deploying program analysis at Facebook.
- From Categorical Logic to Facebook Engineering. LICS 2015: 17-21
- Moving Fast with Software Verification. NASA Formal Methods symposium 2015: 3-11
On the relation between Concurrent Separation Logic and Concurrent Kleene Algebra.
P. O'Hearn, R. L. Petersen, J. Villard and A. Hussain.
J. Log. Algebr. Meth. Program. 84(3): 285-302 (2015)
- 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)