Differences between revisions 6 and 7
Revision 6 as of 2011-02-04 14:18:54
Size: 806
Editor: viktor
Comment:
Revision 7 as of 2011-02-04 14:23:26
Size: 1017
Editor: viktor
Comment:
Deletions are marked like this. Additions are marked like this.
Line 11: Line 11:
=== Table of Contents ===
Line 14: Line 16:
 * [[Decidability]] results
Line 15: Line 18:
 * [[Decidability]] results
=== Editing the wiki ===

To edit the wiki, you will have to create an account and contact [[http://www.mpi-sws.org/~viktor/|Viktor Vafeiadis]] to grant you write permission.

Star wiki

This is a wiki about separation logic.

Separation logic is an extension of Hoare's logic oriented to reasoning about mutable data structures (or, programs with dynamically allocated pointers). It enables more compact proofs and specs of imperative programs than before because of its support for local reasoning, where specifications and proofs concentrate on the portion of memory used by a program component, and not the entire global state of the system.

Table of Contents

Editing the wiki

To edit the wiki, you will have to create an account and contact Viktor Vafeiadis to grant you write permission.

FrontPage (last edited 2013-04-18 12:27:53 by draufer)