@@ -13,21 +13,20 @@ The course is led by Philippa Gardner, with support from Jose Fragoso, Daiva Nau
...
@@ -13,21 +13,20 @@ The course is led by Philippa Gardner, with support from Jose Fragoso, Daiva Nau
As part of the course, [Peter O’Hearn](http://www.pl-enthusiast.net/2015/09/15/facebooks-peter-ohearn-on-programming-languages/) and [Jules Villard](https://www.doc.ic.ac.uk/~jvillar1/) from Facebook came to Imperial College to talk about [Infer](http://fbinfer.com/), an automatic verification tool based on separation logic,
As part of the course, [Peter O’Hearn](http://www.pl-enthusiast.net/2015/09/15/facebooks-peter-ohearn-on-programming-languages/) and [Jules Villard](https://www.doc.ic.ac.uk/~jvillar1/) from Facebook came to Imperial College to talk about [Infer](http://fbinfer.com/), an automatic verification tool based on separation logic,
developed Facebook. At [Facebook](https://www.facebook.com/inferstaticanalyzer/) Infer is used every day to verify millions of lines of code. As well as Facebook, Infer is used by Instagram, kiuwan, oculus, Spotify, UBER, WhatsApp, Marks and Spencer, and Sky.
developed Facebook. At [Facebook](https://www.facebook.com/inferstaticanalyzer/) Infer is used every day to verify millions of lines of code. As well as Facebook, Infer is used by Instagram, kiuwan, oculus, Spotify, UBER, WhatsApp, Marks and Spencer, and Sky.
Infer was [open sourced](https://code.facebook.com/posts/1648953042007882/open-sourcing-facebook-infer-identify-bugs-before-you-ship/) in June 2015.
Infer was [open sourced](https://code.facebook.com/posts/1648953042007882/open-sourcing-facebook-infer-identify-bugs-before-you-ship/) in June 2015. The lab offered students an opportunity to ran Infer on real world Android applications, such as:
[Jules Villard](https://www.doc.ic.ac.uk/~jvillar1/), Software Engineer at Facebook, gave a tutorial on bi-abduction, based on the [slides](/teaching/Bi-Abduction-slides-Sutherland.pdf) that he developed together with Daiva whilst a Post-Doc at Imperial College London.
[Peter O’Hearn](http://www.pl-enthusiast.net/2015/09/15/facebooks-peter-ohearn-on-programming-languages/), Engineering Manager and leader of the Infer team,
gave an overview of the use of Infer at Facebook. Peter, Jules and the Imperial team then ran a lab on how to use Infer, targeting real world Android applications, such as:
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.
[Peter O’Hearn](http://www.pl-enthusiast.net/2015/09/15/facebooks-peter-ohearn-on-programming-languages/), Engineering Manager and leader of the Infer team,
gave an overview of the use of Infer at Facebook. [Jules Villard](https://www.doc.ic.ac.uk/~jvillar1/), Software Engineer at Facebook, gave a tutorial on bi-abduction,
based on the [slides](/teaching/Bi-Abduction-slides-Sutherland.pdf) that he developed together with Daiva whilst a Post-Doc at Imperial College London.
Peter, Jules and the Imperial team then ran the lab on how to use Infer targetting real worl applications. 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.
You can see Lorenzo’s [pull request here.](https://github.com/connectbot/connectbot/pull/448)
You can see Lorenzo’s [pull request here.](https://github.com/connectbot/connectbot/pull/448)
To follow the Infer team, check their [blog](http://fbinfer.com/blog/) or [Twitter](https://twitter.com/fbinfer)
To follow the Infer team, check their [blog](http://fbinfer.com/blog/) or [Twitter](https://twitter.com/fbinfer)
