11th Estonian Winter School in Computer Science (EWSCS)
XI Eesti Arvutiteaduse Talvekool
Palmse, Estonia, March 5-10, 2006
under the auspices of European Educational Forum
John Reynolds
School of Computer Science
Carnegie-Mellon University
Pittsburgh, PA, USA
An Introduction to Separation Logic
Abstract
Separation logic is an extension of Hoare logic for reasoning about programs that use shared resources such as mutable data structures. After defining the semantics and inference rules of the logic, we will illustrate its use in proving programs that manipulate lists and trees. Then, as time permits, we will survey recent developments, such as unrestricted address arithmetic, dynamically allocated arrays, recursive procedures, shared-variable concurrency, and passivity. We will also discuss promising future directions. Some acquaintance with predicate logic and Hoare logic will be assumed.
Course materials
- J. C. Reynolds. Separation logic: a logic for shared mutable data structures. Proc. of 17th Ann. IEEE Symp. on Logic in Computer Science, LICS'02 (Copenhagen, July 2002), pp. 55-74. IEEE CS Press, 2002. Preprint version.
- J. C. Reynolds. A short course on separation logic. Class notes for EWSCS'06. [pdf]
About the Lecturer