Separation Logic

Origin. John Reynolds (2000, 2002) and Peter O'Hearn (2001) extended Hoare logic with spatial connectives for heap reasoning. Builds on Burstall's work and bunched implications (O'Hearn & Pym). Enabled scalable verification of pointer-manipulating programs. Foundation for tools like Infer (Facebook).

Models. Disjoint heap ownership. The separating conjunction P * Q means: the heap can be split into two disjoint parts, one satisfying P and one satisfying Q. Enables local reasoning: verify code by considering only the heap it touches. Frame rule: if code works on a small heap, it works unchanged when embedded in a larger heap.

Formalism.

Heap model:

Heap h: finite partial function from addresses to values
Assertions describe heap and store (variable values)
Disjoint heaps: h₁ ⊥ h₂ means dom(h₁) ∩ dom(h₂) = ∅
Heap combination: h₁ · h₂ defined when h₁ ⊥ h₂

Core assertions:

emp: the heap is empty
E ↦ F: the heap contains exactly one cell, at address E with value F
E ↦ _: cell at E with some value
P * Q: (separating conjunction) heap splits into disjoint parts, one satisfying P, one Q
P — Q:* (magic wand/separating implication) adding a heap satisfying P yields one satisfying Q

Key properties:

P * Q ⊢ Q * P (commutative)
P * emp ⊣⊢ P (emp is unit)
(P * Q) * R ⊣⊢ P * (Q * R) (associative)
P * Q ⊢ P (weakening fails! separation is not strengthening)

Frame rule: {P} C {Q} ──────────── (mod(C) ∩ fv(R) = ∅) {P * R} C {Q * R}

If C is correct for small heap P, it's correct for extended heap P * R, leaving R unchanged. Enables local reasoning.

Small axioms (locality):

{E ↦ _} [E] := F {E ↦ F} (write)
{E ↦ F} x := [E] {E ↦ F ∧ x = F} (read)
{emp} x := alloc(E) {x ↦ E} (allocate)
{E ↦ _} free(E) {emp} (deallocate)

Concurrent separation logic (CSL): Disjoint parallelism: {P₁} C₁ {Q₁} {P₂} C₂ {Q₂} ───────────────────────────── {P₁ * P₂} C₁ ∥ C₂ {Q₁ * Q₂}

Threads with disjoint resources can run in parallel without interference.

Symbols.

Symbol	Unicode	Name	Meaning
*	—	Separating conjunction	Disjoint heap parts
—*	—	Magic wand	Separating implication
↦	U+21A6	Points-to	Heap cell
emp	—	Empty heap	No heap cells
·	—	Heap composition	Combine disjoint heaps
⊥	U+22A5	Disjoint	Domains don't overlap
∥	U+2225	Parallel	Concurrent execution

Metatheory. Soundness with respect to heap semantics. The frame rule is the key to modularity: verify small specs, compose large programs. Completeness is subtle (Lee, O'Hearn, Yang). Decidable fragments exist for shape analysis. Bi-abduction enables automatic inference (Infer tool).

Applies to. Verifying C/C++ pointer programs. Data structure verification (linked lists, trees). Memory safety (use-after-free, double-free). Concurrent programs (CSL, Iris). Rust's ownership model is inspired by separation. Tools: Infer, Verifast, Iris/Coq.

Limitations. Magic wand is hard to reason about in practice. Concurrent separation logic extensions add complexity (rely-guarantee, permissions). Abstraction over data structures requires additional machinery (abstract predicates). Automation is improving but not complete. Garbage-collected languages need different models.