Speaker 1: Professor Peter O’Hearn, Facebook and University College London
Speaker 2: Professor Brad Karp - University College London
Speaker Host: Professor Jon Crowcroft FRS (Science and Programme Committees)
About the event
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
Prior to taking up his post at UCL in late 2005, Karp held joint appointments at Intel Research and Carnegie Mellon, and as a researcher at ICSI at UC Berkeley. He is a recipient of the Royal Society-Wolfson Research Merit Award (2005-2010). He served as program co-chair of ACM SIGCOMM 2015, and as a member of the ACM HotNets Steering Committee from 2009-2014. Karp earned his Ph.D. in Computer Science at Harvard University in 2000, and holds a B.S. in Computer Science from Yale University, earned in 1992.