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). Historically, data structures with embedded pointers caused great difficulty for the tractability of program specifications and proofs using classical techniques (usually based on classical predicate logic). Separation logic uses novel primitives of resource separation to approach this problem, resulting in more concise program specifications and proofs than was possible previously. More generally, the 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.

The purpose of these pages is to provide information 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.

The general context is methods of reasoning about programs. This wiki does not provide background on the general issue, for which the reader can search on the web for such topics as logics of programs, Hoare logic, program verification, and so on.

Table of Contents

• Basics of separation logic

• Prehistory and Early Days

• Concurrent program logics (CSL, RGSep, etc.)

• Context logic

• Abstract predicates

• Decidability results

• Verification tools based on SL

  • SL in proof assistants (Coq,HOL,etc.)

  • Program Analysis based on SL

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.