I am a Professor of Computer Science at University College London and an Engineering Director at Lacework. 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.



  • Finding Real Bugs in Big Programs with Incorrectness Logic   OOPSLA'22
  • 2021 IEEE Cybersecurity Award for Practice     blog     Iverson on practice
  • Facebook's Code Checker.   Computerphile interview video
  • Applying Formal Verification to Microkernel IPC at Meta   CPP'22
  • On Algebra of Program Correctness and Incorrectness.   RAMICS'21
  • Formal Reasoning and the Hacker Way. ICSE'20 keynote.
  • 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 )
  • POPL 2019 Most Influential Paper Award for research that led to Facebook Infer
  • A True Positives Theorem for a Static Race Detector POPL'19
  • RacerD: Compositional Static Race Detection. OOPSLA'18
  • From Start-ups to Scale-ups: Opportunities and Open Problems for Static and Dynamic Program Analysis. M Harman and P O'Hearn. Invited paper at SCAM'18
  • Experience developing and deploying concurrency analysis at Facebook. Invited tutorial at SAS'18
  • Continuous Reasoning: Scaling the impact of formal methods. LICS'18.
  • Concurrent Separation Logic.
    Steve Brookes and Peter O'Hearn. ACM SIGLOG News Vol 3, No 3, pp 47-65, July 2016
  • The essence of Reynolds, paper+talk
  • CurryOn'16 talk on deploying Infer at Facebook.

    email: p.ohearn AT ucl.ac.uk