Continuous Reasoning: Scaling the impact of formal methods

This lecture was recorded: available in our gallery.

Abstract

Formal reasoning about programs is one of the oldest and most fundamental research directions in computer science. It has also been one of the most elusive. There has been a tremendous amount of valuable research in formal methods, but rarely have formal reasoning techniques been deployed as part of the development process of large industrial codebases.

This talk describes work in continuous reasoning, where formal reasoning about a (changing) codebase is done in a fashion which mirrors the iterative, continuous model of software development that is increasingly practiced in industry. We suggest that advances in continuous reasoning will allow formal reasoning to scale to more programs, and more programmers. We describe our experience using continuous reasoning with large, rapidly changing codebases at Facebook, and we describe open problems and directions for research for the scientific community.

This a paper with the same title accompanying this talk appears in the LICS’18 proceedings.

Bio
Peter O’Hearn is a Research Scientist at Facebook, where he works on the science and engineering of reasoning about programs. 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 formal reasoning startup, Monoidics Ltd, which was acquired by Facebook in 2013. The Infer program analyzer developed by Peter’s team runs internally on Facebook’s code bases, resulting in thousands of bugs being fixed before they reach production each month. Infer is also used in production at number of other companies, such as Amazon, Mozilla, Spotify and JD.com. Peter is a Fellow of the UK Royal Academy of Engineering and has received a number of awards for his work, including the 2016 CAV Award and the 2016 Gödel Prize.