Talk videos.
My Journey to the Dark Side.
Talk at POPL'24 workshop on Incorrectness.
AI for the People.
Talk at N40AI: POPL'24 workshop on the next 40 years of Abstract Interpretation.
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.
VIDEO
email: p.ohearn AT ucl.ac.uk