Brief BioPeter O'Hearn is a Research Scientist at Facebook, where he works on the science and engineering of program verification and analysis, including deployment against widely-used industrial products. Peter has done research in the broad areas of programming languages and logic for over 25 years, having held academic positions at Syracuse University, Queen Mary University of London, and University College London (he continues to hold a part-time professorial position at UCL). With John Reynolds he developed separation logic, a theory which opened up new practical possibilities for program proof. In 2009 Peter cofounded a software verification startup company, Monoidics Ltd, which was acquired by Facebook in 2013. The Infer program analyzer developed by Peter's team runs on every modification to the code of Facebook's mobile apps, resulting in hundreds of bugs being fixed before they reach production each month. 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 versionI 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.