From b4b6965023fbb825597dfa13ab36783798f6031e Mon Sep 17 00:00:00 2001 From: Teresa Carbajo-Garcia <t.carbajo-garcia@imperial.ac.uk> Date: Fri, 25 Nov 2016 14:38:29 +0000 Subject: [PATCH] Add new file --- teaching/InferLab.md | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) create mode 100644 teaching/InferLab.md diff --git a/teaching/InferLab.md b/teaching/InferLab.md new file mode 100644 index 0000000..a480358 --- /dev/null +++ b/teaching/InferLab.md @@ -0,0 +1,22 @@ +--- +title: Separation Logic +project_id: sl +menu: true +parent_menu: Teaching +menu_order: 5 +--- +A team from Facebook came run a lab on [Infer[)http://fbinfer.com/), and industrial verification tool developed by a team led by [Peter O’Hearn](http://www.pl-enthusiast.net/2015/09/15/facebooks-peter-ohearn-on-programming-languages/) +Logic MEng and MSc course. +Petar O'Hearn, Engineering Manager at Facebook, and Jules Villard, Software Engineer, gave a tutorial on how to use Infer +- an automatic verification tool based on separation logic. At Facebook, Infer is used every day to verify millions of lines of code. +The tutorial targeted real world Android applications, such as: + - [PocketHub](https://github.com/pockethub/PocketHub) + - [Wikipedia Android app](https://github.com/wikimedia/apps-android-wikipedia) + - [DuckDuckGo](https://github.com/duckduckgo/duckduckgo) + - [k-9 mail client](https://github.com/k9mail/k-9) + +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 + +You can find the slides to the tutorial here + +You can follow the Infer team on their [blog](http://fbinfer.com/blog/) and [Twitter](https://twitter.com/fbinfer) -- GitLab