The Separation Logic course is a 4th-year MEng and MSc course on local reasoning about programs that manipulate the heap at the Department of Computing, Imperial College London. The course is led by Philippa Gardner, with support from Jose Fragoso, Daiva Naudžiūnienė, Azalea Raad and Julian Sutherland.

As part of the course, Peter O’Hearn and Jules Villard from Facebook came to Imperial College to talk about Infer, an automatic verification tool based on separation logic, developed at Facebook. At Facebook, Infer is used every day to verify millions of lines of code. Infer was open sourced in June 2015. As well as Facebook, Infer is used by Instagram, kiuwan, oculus, Spotify, UBER, WhatsApp, Marks and Spencer, and Sky.

Infer Lab Infer Lab

The lab offered students an opportunity to run Infer on real world Android applications, such as:

Peter O’Hearn, Engineering Manager at Facebook and leader of the Infer team, gave an overview of the use of Infer at Facebook. Jules Villard, Software Engineer at Facebook, gave a tutorial on bi-abduction, based on the slides that he developed together with Daiva Naudžiūnienė whilst a Post-Doc at Imperial College London.

Peter, Jules and the Imperial team then showed students at the lab how to use Infer on real worl applications. During the tutorial, one of the students, Lorenzo Paoliani, ran Infer on ConnectBot, an SSH client for Android, and found a resource leak bug. He reported this on github and submitted a pull request for fixing this problem, which has been accepted and now merged. You can see Lorenzo’s pull request here.

Infer Lab

To follow the Infer team, check their blog or Twitter. For more details on the Infer lab or the Separation Logic course, contact the Imperial team below.