Brief Bio

Peter O'Hearn is an Engineering Director at Facebook, where he works on developing and deploying techniques from program verification and analysis. 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. In 2016 he was elected Fellow of the UK Royal Academy of Engineering.

 

Longer version

I am an Engineering Director 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 2013. At Facebook I have been working on developing and deploying techniques from program verification and static analysis.

With David Pym I developed bunched logic, a general logic of resource which was a more abstract cousin of and precursor to separation logic. The work with Reynolds on separation 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 separation 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.