Plenary 9 July
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 reports on work at Facebook where we are developing and deploying formal reasoning using the Infer program analysis platform. Infer’s key features are speed, scale and effectiveness: it is deployed to a codebase with tens of millions of lines of code, which undergoes thousands of code changes per day, in a way that results in thousands of bugs being caught each month before the code reaches production, in products used by over a billion people daily. Our central finding is that by reasoning continuously about the code as it changes, formal reasoning can keep up with the continuous development practice of modern codebases, and as a result can prove effective in a challenging, high-momentum software development situation. We describe the technical innovations that have led to these results, as well as new challenges which could lead to greater impact for the field of formal reasoning.
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.