@@ -15,7 +15,7 @@ In the late 1960s, Tony Hoare developed Hoare logic, a formal system with a set
In 2001, building on Hoare's work and early ideas from Burstall, O'Hearn and Reynolds introduced separation logic, in which the reasoning does scale. This course will provide a whirl-wind tour of separation logic, its verification tools and cutting-edge research on reasoning about concurrent programs.
Separation logic was introduced to reason about shared mutable data structures represented in the heap: in particular, to catch memory overruns and null-pointer dereferencing.
It has been used to reason about C, Java and JavaScript programs, and algorithms for shared-memory concurrency.
There are many academic verification tools, such as Smallfoot, Verifast and Abductor, and the industrial tool [Infer](http://fbinfer.com/), developed by a team led by Peter O'Hearn at Facebook.
There are many academic verification tools, such as [Smallfoot[(http://www0.cs.ucl.ac.uk/staff/p.ohearn/smallfoot/), Verifast and Abductor, and the industrial tool [Infer](http://fbinfer.com/), developed by a team led by Peter O'Hearn at Facebook.
As well as Facebook, Infer is used by Instagram, kiuwan, oculus, Spotify, UBER, WhatsApp, Marks and Spencer, and Sky.
