Separation logic & local reasoning
This is a wiki about separation logic, an extension of Hoare's logic oriented to reasoning about mutable data structures (or, programs with dynamically allocated pointers). Separation logic supports 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. This allows for more concise program specifications and proofs than was possible previously.
The purpose of these pages is to give some context for people wanting to learn about the work. There are subpages covering a number of topics, each of which described key ideas or developments on a subtopic, and several of which contain many further pointers to the literature.
Table of Contents
Concurrent program logics (CSL, RGSep, etc.)
Decidability results
Editing the wiki
To edit the wiki, you first have to create an account and contact Viktor Vafeiadis to grant you write permission. Then, login and click on the "Edit" link to modify a page.