diff --git a/teaching/InferLab.md b/teaching/InferLab.md index 20b4836448d6e806c979e7e26883ece7825f6467..0d6bf6e48f93b7d8dccc499b3fe66ede7e777e55 100644 --- a/teaching/InferLab.md +++ b/teaching/InferLab.md @@ -6,23 +6,31 @@ parent_menu: Teaching menu_order: 5 --- -The [Separation Logic](https://psvg.doc.ic.ac.uk/teaching/separationlogic.html) course is a a 4th-year MEng and MSc course on local reasoning about programs that manipulate the heap at the [Department of Computing](http://www.imperial.ac.uk/computing), [Imperial College London](http://www.imperial.ac.uk). -The course is led by Philippa Gardner, with support from Jose Fragoso, Daiva Naudziuniene, Azalea Raad and Julian Sutherland. +The [Separation Logic](https://psvg.doc.ic.ac.uk/teaching/separationlogic.html) course is a a 4th-year MEng and MSc course +on local reasoning about programs that manipulate the heap at the [Department of Computing](http://www.imperial.ac.uk/computing), +[Imperial College London](http://www.imperial.ac.uk). The course is led by Philippa Gardner, with support from Jose Fragoso, Daiva Naudžiūnienė, +Azalea Raad and Julian Sutherland. + +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 at [Facebook](https://www.facebook.com/inferstaticanalyzer/). +At Facebook, 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.   -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. -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 run Infer on real world Android applications, such as: +The lab offered students an opportunity to run Infer on 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) - -[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 O’Hearn, Engineering Manager at Facebook 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 Naudžiūnienė whilst +a Post-Doc at Imperial College London. 