Deep Reasoning about Big Code - Public Lecture
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, Dr. Peter O'Hearn will describe the reasoning at scale that takes place at Facebook, and 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.
Peter O’Hearn FRS FREng
Research Scientist, Facebook, and Professor of Computer Science, University College London
Peter O’Hearn is a computer scientist who has made major contributions to the science and engineering of program correctness. His research contains a strand stretching from abstract topics such as mathematical logics through to automated analysis of industrial software used regularly by billions of people.
Peter is known particularly for separation logic, a theory which opened up new possibilities for scaling logical reasoning about code. After over 20 years as an academic, Peter took a position at Facebook in 2013 with the acquisition of a startup he cofounded, Monoidics Ltd. The Infer program analyzer, developed by Peter’s team, has resulted in tens of thousands of issues being fixed by Facebook engineers before they reach production. Infer is also used at Amazon, Spotify, Mozilla and other companies.
Peter graduated with a BSc from Dalhousie in 1985, and received an honorary doctorate from Dalhousie in June 2018. He is a fellow of the Royal Society and the Royal Academy of Engineering, and has received a number of awards for his work, including the Computer Aided Verification Award and the Gödel Prize.
Community Interest, Lectures, Seminars, Alumni Events
Room 127, Goldberg Computer Science Building
6050 University Avenue
FreeDeep Reasoning about Big Code - Public Lecture