Peter O’Hearn is a computer scientist who has made major contributions to the science and engineering of program correctness. His research contains a strand stretching from abstract topics such as mathematical logics through to automated analysis of industrial software used regularly by billions of people.
Peter is known particularly for separation logic, a theory he developed with John Reynolds which opened up new possibilities for scaling logical reasoning about code. This built upon prior work of Peter and David Pym on logic for resources.
After over 20 years as an academic, Peter took a position at Facebook in 2013 with the acquisition of a startup he cofounded, Monoidics Ltd. The Infer program analyzer, developed by Peter’s team, has resulted in tens of thousands of issues being fixed by Facebook engineers before they reach production. Infer is also used at Amazon, Spotify, Mozilla and other companies.
Peter is a fellow of the Royal Academy of Engineering (2016) and is the recipient of a number of awards, including the Royal Society Wolfson Research Merit Award (2007), the Computer Aided Verification Award (2016) and the Gödel Prize (2016).
Research Scientist, Facebook Professor of Computer Science, University College London (UCL)