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 — separating conjunction is not weakening. The cell described by Q is still in the heap, and P alone says the heap holds nothing but what P describes. Contrast ordinary ∧, where P ∧ Q ⊢ P always.

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.

Metatheory. Soundness is with respect to the stack-heap model under the tight reading of a triple: from any state satisfying P the command must not fault, and any terminating run must end in a state satisfying Q. Faulting is what makes the frame rule possible, and Yang and O'Hearn (2002) identified the exact condition — the rule is sound for commands that are local, meaning they satisfy safety monotonicity (safe on a small heap implies safe on any extension) and the frame property (an execution on the large heap restricts to one on the small heap). Ishtiaq and O'Hearn (2001) showed the magic wand is not decoration but the mechanism of backward reasoning: the weakest precondition of [E] := F for Q is (E ↦ _) * ((E ↦ F) —* Q), so wp is expressible only because —* is in the language. Calcagno, Yang, and O'Hearn (2001) settled decidability: the quantifier-free assertion language with ↦, , and — is decidable and PSPACE-complete, while adding first-order quantification over addresses makes validity undecidable. The symbolic-heap fragment with points-to and list segments admits polynomial-time entailment, which is what makes shape analysis tractable, and bi-abduction — solving P * ?antiframe ⊢ Q * ?frame — is the inference step that lets Infer analyse each procedure without a whole-program precondition.

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. The frame rule is not free: it holds only for local commands, and ordinary language features destroy locality. A deterministic allocator that always returns the least free address violates the frame property, since the same code run on a larger heap returns a different address; so does any primitive that can observe the whole heap, such as a dispose-everything operation or unrestricted address arithmetic. The frame rule's side condition mod(C) ∩ fv(R) = ∅ also means stack variables are outside the separating discipline unless variables are themselves treated as resource. Decidability is bounded on both sides: quantifier-free entailment is already PSPACE-complete, quantification over addresses makes validity undecidable, and entailment between symbolic heaps with arbitrary user-supplied inductive predicates is undecidable. The tight interpretation forbids leaked cells, so garbage-collected languages need a different, intuitionistic reading in which leak-freedom becomes inexpressible. Loop invariants remain unautomated, and the relative-completeness caveat inherited from Hoare logic is unchanged.

© 2026 Lingenic LLC