A BRICS Mini-Course
November 11, 13, 18, 20, 25 and 27, December 2 and 4, 2003
John C. Reynolds, John.Reynolds@cs.cmu.edu
School of Computer Science, Carnegie Mellon University, Pittsburgh, USA
Separation logic is an extension of Hoare logic for reasoning about programs that use shared mutable data structures. We will survey the current development of this logic, including extensions that permit unrestricted address arithmetic, dynamically allocated arrays, recursive procedures, and shared-variable concurrency. We will also discuss promising future directions.
Some acquaintance with predicate logic will be assumed.