CIDEC ÜIK |
Estonian Winter Schools in Computer Science Eesti arvutiteaduse talvekoolid |
EWSCS 2006 EATTK 2006 |

XI Eesti Arvutiteaduse Talvekool

School of Computer Science

Carnegie-Mellon University

Pittsburgh, PA, USA

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.

- 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]

http://www.cs.ioc.ee/yik/schools/win2006/

Modified Apr 30, 2013 11:38 by ewscs06(at)cs.ioc.ee