diff --git a/_posts/2016-11-14-inferlab.md b/_posts/2016-11-14-inferlab.md new file mode 100644 index 0000000000000000000000000000000000000000..d4aa18c7d74d5bb78b789ffb4a561141ecb20da1 --- /dev/null +++ b/_posts/2016-11-14-inferlab.md @@ -0,0 +1,11 @@ +--- +title: OFacebook runs lab on Infer, industrial verification tool +--- + +[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 MEng and MSc course (404H). +Infer, an automatic verification tool based on separation logic, 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](https://gitlab.doc.ic.ac.uk/resource-reasoning/psvg.doc.ic.ac.uk/blob/master/teaching/InferLab.md) Lab page.