Keynote: Underapproximate Reasoning at Scale

Abstract

I recount lessons learned from a decade of experience in industry on logical methods for reasoning about programs at scale. It started with the shock of bumping program reasoning, usually a “move slow and break nothing” approach,  up against fast-paced industrial software development practices. Gradually, I came to appreciate the importance of proving the presence of bugs as well as the much rarer case of proving their absence, and together with many colleagues I sought foundations for and applications of under-approximate reasoning at scale. New tools and theories and tools were developed including RacerD, an under-approximate data race detector, Pulse, a new compositional engine for the Infer tool, and Incorrectness Logic. As well as describing some of the above I hope to convey both technical opportunities and scientific challenges in underapproximate reasoning at scale.

Presenter Bio

Peter O'Hearn is an Engineer at Lacework and a Professor at University College London. Peter has done research in the broad areas of programming languages and logic, and held academic positions at Syracuse University, Queen Mary University of London, and University College London, and he worked at Facebook from 2013-2021; he joined FB with the acquisition of the verification startup Monoidics. With John Reynolds Peter devised Separation Logic, a theory which opened up new practical possibilities for program proof, including the technology which led to the Infer program analyzer developed by Peter's team at Facebook. Infer runs internally on Facebook's code bases, and has detected hundreds of thousands of bugs which have been fixed by Facebook's developers before reaching products. Infer is also used in production at number of other companies, including Amazon, Microsoft and Mozilla, and is deployed to many other organizations through the Sonatype Lift analysis platform. Most recently Peter developed Incorrectness Logic, a theory aimed at providing a foundation for bug catching tools based on proofs of the presence of bugs. Peter is a Fellow of the Royal Society (elected 2018), a Fellow of the Royal Academy of Engineering (2016), he has received a number of awards for his work including the the 2016 G\"odel Prize, the 2016 CAV Award, the 2021 IEEE Cybersecurity Award for Practice, and he received an honorary doctorate from Dalhousie University in 2018.