Skip to content
Snippets Groups Projects
Commit 289bdf48 authored by Teresa Carbajo-Garcia's avatar Teresa Carbajo-Garcia
Browse files

Update 2016-11-14-inferlab.md

parent 00302b93
No related branches found
No related tags found
No related merge requests found
......@@ -2,13 +2,19 @@
title: Facebook runs lab on Infer, industrial verification tool
---
The [Separation Logic](https://psvg.doc.ic.ac.uk/teaching/separationlogic.html) course team ran a lab on Infer,
an automatic verification tool based on separation logic, developed at [Facebook](https://www.facebook.com/inferstaticanalyzer/)
where it is used every day to verify millions of lines of code.
[Peter O’Hearn](http://www.pl-enthusiast.net/2015/09/15/facebooks-peter-ohearn-on-programming-languages/),
Engineering Manager, and [Jules Villard](https://www.doc.ic.ac.uk/~jvillar1/), Software Engineer at Facebook,
gave a tutorial on how to use [Infer](http://fbinfer.com/) to the students on the [Separation Logic](https://psvg.doc.ic.ac.uk/teaching/separationlogic.html) MEng and MSc course (404H).
Engineering Manager and leader of the Infer team, gave an overview of the use of Infer at Facebook. and [Jules Villard](https://www.doc.ic.ac.uk/~jvillar1/),
Software Engineer at Facebook, gave a tutorial on how to use [Infer](http://fbinfer.com/). 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](/images/posts/Infer-lab-1.jpg)
Infer is an automatic verification tool based on separation logic and was developed at Facebook by a team
led by Peter O’Hearn. At [Facebook](https://www.facebook.com/inferstaticanalyzer/), Infer is used every day to verify millions of lines of code.
The tutorial targeted real world Android applications, such as PocketHub, Wikipedia Android app,
DuckDuckGo and k-9 mail client. For more details and slides, see the [Infer Lab](https://psvg.doc.ic.ac.uk/teaching/InferLab.html) page.
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](https://psvg.doc.ic.ac.uk/teaching/InferLab.html) page.
\ No newline at end of file
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment