diff --git a/teaching/InferLab.md b/teaching/InferLab.md new file mode 100644 index 0000000000000000000000000000000000000000..a480358b30e7f7876eb3aa048fe175a7d8c73fc8 --- /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)