I am a Professor of Computer Science at University College London and a Researcher at Meta AI (FAIR).
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:
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
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.
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
