Estonian Winter Schools in Computer Science    
Eesti arvutiteaduse talvekoolid
EWSCS 2006
EATTK 2006

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


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

About the Lecturer


Modified Apr 30, 2013 11:38 by ewscs06(at)