##master-page:FrontPage
#format wiki
#language en
#pragma section-numbers off
= 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).  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 general context of the work is methods for 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 ===

 * [[SeparationLogic|Basics of separation logic]] 
 * [[EarlyDays|Prehistory and Early Days]] 
 * [[Concurrency|Concurrent program logics]] (CSL, RGSep, etc.) 
 * [[ContextLogic|Context logic]]
 * [[AbstractPredicates|Abstract predicates]]
 * [[Decidability]] results
 * [[ToolSupport|Verification tools based on SL]]
  * [[SLInProofAssistants|SL in proof assistants (Coq,HOL,etc.)]]
  * [[SLInProgramAnalysis|Program Analysis based on SL]]

=== Editing the wiki ===

To edit the wiki, you have to contact [[http://www.mpi-sws.org/~viktor/|Viktor Vafeiadis]] to get an account. Then, login and click on the "Edit" link to modify a page.