@@ -11,8 +11,7 @@ The Scalable Software Verification course (formerly Separation Logic)is a 4th ye
#### Description of the Course
In the late 1960s, Tony Hoare developed Hoare logic, a formal system with a set of rules for reasoning rigorously about the correctness of imperative programs that alter the variable state. However, Hoare logic is not good at reasoning about imperative programs that alter the heap state, since the reasoning does not scale.
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.
In the late 1960s, Tony Hoare developed Hoare logic, a formal system with a set of rules for reasoning rigorously about the correctness of imperative programs that alter the variable state. However, Hoare logic is not good at reasoning about imperative programs that alter the heap state, since the reasoning does not scale. 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.
