Brief Bio

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 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.

 

Longer version

I am a Research Scientist at Facebook and a Professor of Computer Science at University College London. My work has been in the broad areas of programming languages and logic, ranging from new logics and mathematical models to industrial applications of program proof. With John Reynolds I developed Separation Logic, a theory which opened up new practical possibilities for program proof. In 2009 I cofounded a software verification startup company, Monoidics Ltd, which was acquired by Facebook in 2017 at which point I moved to Facebook with the Monoidics engineering team where I led the Infer program analys team, which deployed a novel program analyzer that catches thousands of bugs/month which are fixed by Facebook's engineers before they reach production. In 2017 I moved from a management (Director) role back to a technical role, to pursue problems in program verification and static analysis, particularly concurrency analysis at scale. I led the Infer team at Facebook up to 2017 --

I have developed several new logics. The Bunched Logic of David Pym and I is a general logic of resource, a more abstract cousin of and precursor to separation logic. The work with Reynolds on Leparation Logic extended Hoare's logic to address the problem of tractable reasoning about the mutation of data structures in computer memory; during this work I invented a theory of local reasoning where specifications and proofs mention only the resources (memory, files, etc) accessed by program components, and this led to a significant increase in the scalability of automated reasoning applied to large codebases. Then I proposed a Concurrent Ceparation Logic, which has made inroads on the problem of modular reasoning about shared-memory concurrent programs.

These theoretical advances led to new software tools research. The Smallfoot tool (Calcagno, Berdine and I, 2002-2005) showed how to do automatic program verification with separation logic, where specifications concentrate on the footprints of program components. Next, Space Invader (Calcagno, Distefano, Yang and I, 2006-2008) advanced an automatic program analysis where abstract interpretation paired with separation logic proof theory was used to automatically prove memory-safety properties of dmsll (up to 10k LOC) complete programs. Then, Abductor (again Calcagno, Distefano, Yang and I, JACM'11) achieved an extreme modular program analysis based on the local reasoning idea, where the footprints of program program components were calculated (approximated) without requiring analysis of the complete program; this allowed the analysis to scale to millions of lines of code, and to work incrementally on code changes. This extreme modular analysis was the basis of the industrial program analyzer Infer from Monoidics, which is now being developed at Facebook.

I did my PhD (graduated 1991) at Queen's University in Kingston, Ontario, Canada, under the supervision of Bob Tennent. I held academic positions at Syracuse (1991-1995) and Queen Mary University of London (1996-2012), before moving to University College London in March of 2012. I have been the recipient of an EPSRC Advanced Research Fellowship, a Royal Society Wolfson Research Merit Award, a Most Influential POPL Paper Award, and a Royal Academy of Engineering/Microsoft Research Chair. I was co-recipient of the 2016 CAV Award for work on separaiton logic and its automation, and the 2016 Gödel Prize for the discovery of concurrent separation logic. I was elected Fellow of the Royal Academy of Engineering in 2016.