BioPeter 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 has received a number of awards for his work, including the 2011 POPL Influential Paper Award, the 2016 CAV Award and the 2016 Gödel Prize. Peter is a Fellow of the Royal Society, a Fellow of the Royal Academy of Engineering, and he received an honorary doctorate from Dalhousie University in 2018.