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.

It introduces a new logical connective, *, called separating conjunction and proof rules for handling heap-manipulating commands. 

latex error! exitcode was 1 (signal 0), transscript follows:

This is pdfTeX, Version 3.14159265-2.6-1.40.19 (TeX Live 2019/dev/Debian) (preloaded format=latex)
entering extended mode
(./latex_1776dec153fdb715732200b23bea4f5cab47e32d_p.tex
LaTeX2e <2018-12-01>
(/usr/share/texlive/texmf-dist/tex/latex/base/article.cls
Document Class: article 2018/09/03 v1.4i Standard LaTeX document class
(/usr/share/texlive/texmf-dist/tex/latex/base/size12.clo))
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty))
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty
For additional information on amsmath, use the `?' option.
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty))
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty))
(/usr/share/texlive/texmf-dist/tex/latex/amscls/amsthm.sty)
(/usr/share/texlive/texmf-dist/tex/latex/base/inputenc.sty)
No file latex_1776dec153fdb715732200b23bea4f5cab47e32d_p.aux.
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd)
! Missing $ inserted.
<inserted text> 
                $
l.10 ...nd $h_1 \models P_1$ and $h_2 \models P_2}
                                                  $
! Extra }, or forgotten $.
\mbox #1->\leavevmode \hbox {#1}
                                
l.10 ...nd $h_1 \models P_1$ and $h_2 \models P_2}
                                                  $
! Improper \prevdepth.
\newpage ...everypar {}\fi \par \ifdim \prevdepth 
                                                  >\z@ \vskip -\ifdim \prevd...
l.11 \end{document}
                   
! Missing } inserted.
<inserted text> 
                }
l.11 \end{document}
                   
! Missing $ inserted.
<inserted text> 
                $
l.11 \end{document}
                   

Overfull \hbox (103.40036pt too wide) in paragraph at lines 10--11
[]$[]$ 
[1] (./latex_1776dec153fdb715732200b23bea4f5cab47e32d_p.aux) )
(see the transcript file for additional information)
Output written on latex_1776dec153fdb715732200b23bea4f5cab47e32d_p.dvi (1 page,
 568 bytes).
Transcript written on latex_1776dec153fdb715732200b23bea4f5cab47e32d_p.log.

The most prominent proof rule is the frame rule:

$$\frac{ \{P\}~C\{Q\} }{ \{P*F\}~C\{Q*F\} }\quad \mathbf{fv}(F)\cap\mathbf{mod}(C) = \emptyset$$

This says that a program that runs correctly with a heap satifying its precondition also runs correctly with a bigger initial heap. Further, it is guaranteed not to touch the additional portion heap.

The best way to start is to read the following survey paper by John Reynolds:

Separation Logic: A Logic for Shared Mutable Data Structures. JC Reynolds. In LICS 2002.

Extensions of separation logic have been devised to better handle:

Separation logic has also been extensively used in semi-automatic and automatic program analyses (often known as shape analyses) for proving functional correctness of programs or simply the absence of certain kinds of runtime errors and/or memory leaks.

ToolSupport