Brief bio. I am a Researcher at Meta Superintelligence Labs and a Professor at University College London. I developed Separation Logic and Incorrectness Logic, which underpin tools like Infer, used to detect hundreds of thousands of bugs at Facebook, Microsoft, and Amazon. I co-founded Monoidics (acquired by Facebook) and am a Fellow of the Royal Society and recipient of the Gödel Prize.

I'm interested in "reasoning", both for code and for other-than-code. 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, and I try to do theory and engineering at the same time or at least interleaved.

Recent

  • LLMs versus the Halting Problem   Draft paper, 2026
  • Logic.py: Bridging the Gap between LLMs and Constraint Solvers   NeurIPS'26
  • Harden and Catch for Just-in-Time Assured LLM-Based Software Testing: Open Research Challenges   FSE'25
  • Non-termination Proving at Scale   OOPSLA'24
  • Applying Formal Verification to Microkernel IPC at Meta   CPP'22
  • Finding Real Bugs in Big Programs with Incorrectness Logic   OOPSLA'22

    Selected High Level articles and Talks

  • Incorrectness Logic. POPL'20. errata (typos).   Video of talk
  • Scaling Static Analyses at Facebook. Communications of the ACM, Volume 62 Issue 8, August 2019, Pages 62-70.
  • Separation Logic. Communications of the ACM, February 2019, Vol. 62 No. 2, Pages 86-95. ( Appendix on Mechanized Reasoning )
  • Concurrent Separation Logic.
    Steve Brookes and Peter O'Hearn. ACM SIGLOG News Vol 3, No 3, pp 47-65, July 2016
  • Facebook's Code Checker.   Computerphile interview video
  • CurryOn'16 talk on deploying Infer at Facebook.

    email: p.ohearn AT ucl.ac.uk