The Separation Logic course team ran a lab on Infer, an automatic verification tool based on separation logic, developed at Facebook where it is used every day to verify millions of lines of code.

Peter O’Hearn, Engineering Manager and leader of the Infer team, came to talk about 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.

The Imperial team then ran a lab on how to use Infer to verify real world Android applications, using as examples PocketHub, Wikipedia Android app, DuckDuckGo and k-9 mail client. During the tutorial, one of the students, Lorenzo Paoliani, ran Infer on ConnectBot, an SSH client for Android, and found several null dereference bugs. He reported this on github and submitted a pull request for fixing that problem, which has been accepted and now merged.

For more details and slides, see the Infer Lab 2016 page.