Estonian Winter Schools in Computer Science
Eesti arvutiteaduse talvekoolid
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.
Modified Apr 30, 2013 11:38 by ewscs06(at)cs.ioc.ee