Speaker 1: Professor Peter O’Hearn, Facebook and University College London Website]
Speaker 2: Professor Brad Karp – University College London Website]
Dates: April 27, 2016
Speaker Host: Professor Jon Crowcroft FRS (Science and Programme Committees)
Speaker 1: Professor Peter O’Hearn, Facebook & UCL
Reasoning with Big Code
Organisations are increasingly relying on large, evolving code bases, often involving many millions of lines of code undergoing rapid concurrent modification. Keeping the code in shape is critical to the organisations that rely on it, and this presents considerable engineering and scientific challenges. Reasoning of different forms (spanning static and dynamic verification) plays a crucial role. In this talk I will describe the reasoning at scale that we do at Facebook, and I will relay some of the experiences of deploying a static analyser that uses logical reasoning and yet works at a velocity consistent with Facebook’s fast-paced engineering culture. I will also outline what I think are some of the research opportunities and challenges posed by big code.
Peter O’Hearn is an Engineering Manager at Facebook and a Professor of Computer Science at UCL. His research 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 he developed separation logic, a theory which opened up new practical possibilities for program proof. In 2009 he cofounded a software verification startup company, Monoidics Ltd, which was acquired by Facebook in 2013. The Facebook Infer program analyzer, developed by Peter’s team and recently open-sourced, runs on every modification to the code of Facebook’s mobile apps, in a typical month issuing millions of calls to a custom separation logic theorem prover and catching hundreds of bugs before they reach production.
Speaker 2: Professor Brad Karp, University College London
Safeguarding Users’ Sensitive Data in the Cloud and the Browser