I am a Professor of Computer Science at University College London and an Engineering Director at
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
2021 IEEE Cybersecurity Award for Practice
Iverson on practice
Facebook's Code Checker.
Computerphile interview video
Applying Formal Verification to Microkernel IPC at
On Algebra of Program Correctness and Incorrectness.
Formal Reasoning and the Hacker Way.
Video of talk
Scaling Static Analyses at Facebook.
Communications of the ACM, Volume 62 Issue 8, August 2019, Pages 62-70.
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
RacerD: Compositional Static Race Detection.
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.
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