Skip to content
Snippets Groups Projects
Select Git revision
  • master default
  • fix-bibtex-unicode-filter
  • dataspy-hacking
3 results
Blame Permalink
Forked from Verified Software / psvg.doc.ic.ac.uk
1087 commits behind the upstream repository.
2016-11-14-inferlab.md 1.50 KiB 
title: Facebook runs lab on Infer, industrial verification tool

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, gave an overview of the use of Infer at Facebook. and Jules Villard, Software Engineer at Facebook, gave a tutorial on how to use Infer. 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.

Infer Lab

Then the Imperial team ran a lab on how to use Infer, targeting real world Android applications,such as 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 this problem, which has been accepted and now merged.

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