Peter O’Hearn

Research Scientist

I am a Research Scientist working with the Static Analysis Tools team in the Facebook London Engineering office. I came to Facebook in 2013 with the acquisition of the verification startup Monoidics, and before that I held academic positions at Syracuse University, Queen Mary University of London and University College London. I maintain a part-time Professor position at UCL.

My research has been in the broad areas of programming languages and logic, ranging from new logics and mathematical models to industrial applications of formal proof. With John Reynolds I developed separation logic, a theory which opened up new practical possibilities for program verification. Subsequent work in academic program analysis eventually led to the the Monoidics/Facebook Infer program analyzer, which is notable for supporting deep reasoning about big code that is undergoing rapid concurrent modification. Infer currently runs in production at Facebook, where it helps thousands of bugs be fixed each month before reaching production.

I have received a number of awards for my work in verification including the 2016 CAV Award and the 2016 Godel Prize. I was elected fellow of the Royal Society in 2018 and Fellow of the Royal Academy of Engineering in 2016.

Latest Publications

RAMICS - November 2, 2021

On Algebra of Program Correctness and Incorrectness

Bernhard Möller, Peter O'Hearn, Tony Hoare

POPL - January 23, 2020

Incorrectness Logic

Peter O'Hearn

CACM - July 29, 2019

Scaling Static Analyses at Facebook

Dino Distefano, Manuel Fahndrich, Francesco Logozzo, Peter O'Hearn

CACM - February 1, 2019

Separation Logic

Peter O'Hearn

POPL - January 14, 2019

A True Positives Theorem for a Static Race Detector

Nikos Gorogiannis, Peter O'Hearn, Ilya Sergey

OOPSLA 2018 - November 3, 2018

RacerD: Compositional Static Race Detection

Sam Blackshear, Nikos Gorogiannis, Peter O'Hearn, Ilya Sergey

LICS - August 13, 2015

From Categorical Logic to Facebook Engineering

Peter O'Hearn

February 10, 2015

Moving Fast with Software Verification

Cristiano Calcagno, Dino Distefano, Jeremy Dubreil, Dominik Gabi, Pieter Hooimeijer, Martino Luca, Peter O'Hearn, Irene Papakonstantinou, Jim Purbrick, Dulma Churchill

POPL - January 22, 2014

The Essence of Reynolds

Stephen Brookes, Peter O'Hearn, Uday S. Reddy

Downloads & Projects

View all Downloads & Projects

Infer is a static analysis tool used to detect bugs in Java and C/C++/Objective-C code before it ships.