Separation Logic
Hoare logic
is a triumph — for programs that only push around simple variables. Point it at a program with
pointers and it starts to groan. The trouble is aliasing: two different
expressions, x and y, might name the same memory cell, and then an
innocent-looking [x] := 4 can silently change the value you thought was stored at y.
Suddenly every assertion about the heap must fret about every other pointer that might alias it,
and proofs balloon into unreadable case-splits.
Separation logic — John Reynolds, Peter O'Hearn and Hongseok Yang, around 2001–2002 — is
an extension of Hoare logic built to reason about the heap and pointers locally. Its one great
idea is a new connective that lets an assertion say "these two chunks of memory are separate", so
you can reason about one chunk while blissfully ignoring the rest. It is the logic behind the tools that
verify real, pointer-manipulating C.
The heap and the points-to assertion
Separation logic splits program state into two parts: the store (variables → values,
as before) and the heap (addresses → values, a finite partial function modelling
allocated memory). Assertions now describe the heap, and the atomic building block is the
points-to assertion:
x \mapsto v
read "the heap consists of exactly one cell, at address x, holding
value v." That word exactly is the crux: x \mapsto v
is not just "cell x holds v" — it also asserts the
heap has nothing else in it. Ownership is baked into the assertion. The empty heap is written
\mathsf{emp}.
The figure shows a three-node linked list on the heap. Each box is one cell holding a
[value | next-pointer] pair; the arrows are the next links, and the last points to
\mathsf{nil}. The shading marks two disjoint regions — the subject of
the next section.
The separating conjunction P ∗ Q
Ordinary conjunction P \wedge Q says P and Q both describe the same
heap. Separation logic adds a new one, the separating conjunction:
P * Q
holds of a heap h exactly when h can be
split into two disjoint parts h = h_1 \uplus h_2 with
P holding of h_1 and Q of
h_2. The \uplus demands the two parts have
no address in common.
So x \mapsto 3 \,*\, y \mapsto 4 asserts two cells, at
x and y, holding 3 and 4 — and, for free,
that x \ne y, because disjointness forbids them coinciding. That single
connective is what banishes aliasing: separation is written into the assertion, not reasoned
about after the fact. Note the difference from ordinary conjunction:
x \mapsto 3 \,\wedge\, x \mapsto 3 is fine (one cell, described twice), but
x \mapsto 3 \,*\, x \mapsto 3 is unsatisfiable — you cannot split one
cell into two disjoint cells.
The frame rule: local reasoning
The whole payoff arrives in one inference rule — the reason separation logic exists — the
frame rule:
\dfrac{\{P\}\; C \;\{Q\}}{\{P * R\}\; C \;\{Q * R\}}
provided C modifies no variable free in R. If
C is correct operating on the little heap P, then
it is correct on a bigger heap P * R, leaving the extra part
R — the frame — completely untouched.
This is local reasoning, and it is transformative. You verify a routine against the
small footprint it actually touches — the two cells it swaps, say — and the frame rule
automatically lifts that proof to any larger heap the routine might be dropped into. Contrast Hoare logic,
where a global heap assertion must be threaded through every step. Here, "what the code doesn't touch, the
proof doesn't mention." Modularity, as a logical rule.
It can — and that is exactly the disaster separation logic avoids. To reason about a routine touching
k heap cells in classic Hoare logic, you must state, for every pair of the cells
in scope, whether they alias — a quadratic pile of x_i \ne x_j disequalities
that grows with the whole program's pointers, not just the ones this routine uses. Worse, the
frame — everything the routine doesn't touch — must be re-proved unchanged by hand at every step.
The separating conjunction folds all of that disjointness into the single symbol
*, and the frame rule discharges the "unchanged" obligation once and for all.
The gain isn't cosmetic: it is the difference between proofs that scale to real heap data structures and
proofs that don't.
Reasoning about linked lists
Heap predicates are defined by recursion, mirroring the data structure. "A linked list from
x holding the sequence \alpha" is:
\mathsf{list}(x, \alpha) \;\equiv\;
\begin{cases}
x = \mathsf{nil} \,\wedge\, \mathsf{emp} & \alpha = [\,] \\[4pt]
\exists v, t.\; x \mapsto (a, t) \,*\, \mathsf{list}(t, \alpha') & \alpha = a\!::\!\alpha'
\end{cases}
Look at the *: the head cell x \mapsto (a, t) is
separate from the rest of the list \mathsf{list}(t, \alpha') — which is
precisely the statement that a well-formed list has no cycles or sharing. Disjointness,
for free, from the connective. Verifying in-place list reversal becomes a clean induction
with the loop invariant "the already-reversed prefix and the yet-to-process suffix are two
separate lists," \mathsf{list}(p, \text{rev}(\sigma)) * \mathsf{list}(q, \tau)
— the * guaranteeing the two segments never accidentally alias as you splice
pointers.
// In-place reversal. Invariant: list(prev, rev(done)) ∗ list(curr, todo)
// — the two segments are always SEPARATE heaps (that ∗ is the whole proof).
function reverse(head: Node | null): Node | null {
let prev: Node | null = null; // reversed prefix
let curr: Node | null = head; // suffix still to process
while (curr !== null) {
const next = curr.next; // remember the rest
curr.next = prev; // splice this node onto the reversed prefix
prev = curr; // grow the prefix
curr = next; // advance into the suffix
}
return prev; // prev now heads the fully reversed list
}
The single most common error is reading * as if it were \wedge.
They are genuinely different connectives. P \wedge Q says P and Q both hold
of the same heap — total overlap allowed. P * Q says the heap splits
into two disjoint pieces, one for each — zero overlap allowed. Concretely,
x \mapsto 3 \,\wedge\, y \mapsto 4 is satisfiable with
x = y (both clauses describing the one cell, which would then need to hold both
3 and 4 — actually unsatisfiable here) whereas x \mapsto 3 \,*\, y \mapsto 4
forces x \ne y outright. And P * P is emphatically
not P: (x \mapsto 3) * (x \mapsto 3) is
unsatisfiable, because one cell cannot be split into two disjoint copies of itself. The star is
multiplicative, consuming resources; ordinary \wedge is idempotent.
Confuse the two and your proof will "prove" impossible aliasings.
Onward: concurrency
Separation logic's greatest hit came from concurrency. Concurrent separation logic
(O'Hearn, 2007 — a Gödel Prize winner) extends the disjointness idea to threads: if two threads operate on
separate heap regions, they cannot interfere, so their proofs simply compose —
\dfrac{\{P_1\}\,C_1\,\{Q_1\} \quad \{P_2\}\,C_2\,\{Q_2\}}{\{P_1 * P_2\}\; C_1 \,\|\, C_2 \;\{Q_1 * Q_2\}}.
The separating conjunction is exactly the statement "no
shared mutable state, so no
data race." This line of work underpins industrial tools — Facebook/Meta's Infer analyses
millions of lines of production code for pointer and concurrency bugs using separation logic under the
hood. One connective, from disjoint list cells all the way to race-free threads.