diff --git a/_posts/2016-11-14-inferlab.md b/_posts/2016-11-14-inferlab.md index ee6e61107bf28e5820d4b048e3c7a5c36b6fd1c4..aa42ac2f10d4fb3104ea03c11dfe249841ed1318 100644 --- a/_posts/2016-11-14-inferlab.md +++ b/_posts/2016-11-14-inferlab.md @@ -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 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