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

 

Recent:

  • Incorrectness and Underapproximation, Semantic Foundations. Slides from part of joint POPL'23 tutorial with A Raad, Q Le, J Vanegue.
  • Finding Real Bugs in Big Programs with Incorrectness Logic   OOPSLA'22. Distinguished Paper Award
  • 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 )
  • 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