How and Why Separation Logic is good for Resource Reasoning about Programs

Separation logic, invented by John C. Reynolds and Peter O'Hearn, has proven to be an effective formalism for the analysis of programs that manipulate memory (in the form of pointers, heaps, stacks, etc.). In addition to the standard propositional connectives, the most important feature of separation logic is its separating conjunction ($A*B$) which holds for a portion of memory, a heap $h$, iff $h$ can be split into separate $h_1$ and $h_2$ so that $A$ holds for $h_1$ and $B$ holds for $h_2$.
In my talk I will address the following issues.
1. General separation models, and concrete heap-like models of practical interest.
2. In-place reasoning, the frame property, the weakest preconditions, inductive definitions (linked lists, trees), within separation logic used as an extension of Hoare logic.
3. As for the assertion language of separation logic, even purely propositional separation logic turns out to be undecidable. What is more, whatever concrete heap-like model $H$ we take, it is undecidable whether a purely propositional formula $A$ is valid in this model $H$. A number of propositional systems which approximate separation logic are undecidable as well. In particular, these include both Boolean BI and Classical BI. Oddly enough, Intuitionistic BI is still decidable.
4. Abduction, the problem of discovering hypotheses that support a conclusion, has mainly been studied in the context of philosophical logic and AI. Recently, the abduction principle — given $A$ and $B$, find a non-trivial $X$ such that $A*X$ entails $B$, is one of the powerful practical tools for iterated deduction and hypothesis formation to ‘dig information out of bare code’. We study the complexity of abduction for a relevant fragment of separation logic over ‘symbolic heaps’ which include a basic ‘points-to’ predicate, and an inductive predicate for describing linked-list segments. Standard entailment turns out to be decidable in polytime, while abduction ranges from NP-complete to polytime for different sub-problems. The following parametrized complexity is of great practical and theoretical importance — that is, the NP-completeness notwithstanding, there is a polytime procedure for finding a solution to abduction but degree of the polynomial is proportional to the number of ‘list segment’ subformulas in $B$.