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 [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 course is led by Philippa Gardner, with support from Jose Fragoso, Daiva Naudziuniene, 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 run a lab on [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 run a lab on [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.
...
@@ -32,6 +32,4 @@ You can see Lorenzo’s [pull request here.](https://github.com/connectbot/conne
...
@@ -32,6 +32,4 @@ You can see Lorenzo’s [pull request here.](https://github.com/connectbot/conne
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)
For more details on the lab, contac the Imperial team
