Separation logic extends Hoare logic with spatial connectives for reasoning about programs that manipulate heap memory. Its central operator, the separating conjunction P * Q, asserts that the heap can be split into two disjoint parts, one satisfying P and the other satisfying Q. This enables local reasoning: a specification for a function describes only the heap fragment the function touches, and the frame rule automatically extends this to any larger heap. Separation logic makes it practical to verify pointer-manipulating programs — linked lists, trees, graphs — that are intractable in standard Hoare logic.
Standard Hoare logic works well for programs that manipulate simple variables, but it struggles with heap-manipulating programs. The root problem is aliasing: when two pointers might refer to the same memory cell, modifying one might silently modify the other. In standard logic, you must track all possible aliasing relationships, leading to a combinatorial explosion. Separation logic, introduced by John Reynolds and Peter O'Hearn around 2000, solves this with a new logical connective designed specifically for heap reasoning.
The key innovation is the separating conjunction, written P * Q. It asserts that the current heap can be partitioned into two disjoint sub-heaps, one satisfying P and the other satisfying Q. The points-to predicate x -> v says that address x holds value v and nothing else is in the heap (it describes a single-cell heap). So x -> 5 * y -> 7 means x points to 5, y points to 7, and crucially x != y because the heaps are disjoint. Non-aliasing is baked into the logic's structure rather than stated as a side condition.
The most powerful consequence is the frame rule: if {P} C {Q} holds, then {P * R} C {Q * R} holds for any frame R whose free variables are not modified by C. This enables local reasoning — you write a specification mentioning only the heap cells the function actually touches (its "footprint"), and the frame rule automatically extends correctness to any larger heap. A linked-list reversal function only needs to specify the list it reverses; the frame rule guarantees it leaves all other heap data untouched. This modularity is what makes separation logic scale to large programs: you verify each component against its small footprint and compose the results.
Separation logic has had enormous practical impact. Facebook's Infer (now Meta's) analyzes millions of lines of C, C++, Java, and Objective-C code using a separation logic engine, automatically finding memory safety bugs like null dereferences, use-after-free, and resource leaks. Concurrent separation logic extends the framework to multi-threaded programs by treating the separating conjunction as an ownership discipline: if thread A owns heap region P and thread B owns region Q, and P * Q holds, the threads cannot interfere because they operate on disjoint memory. This insight connects separation logic to type-theoretic notions of ownership, as seen in Rust's borrow checker, which enforces similar discipline at the type level.
The practical workflow mirrors Floyd-Hoare verification but with spatial assertions. The programmer annotates functions with pre/postconditions expressed in separation logic (describing the shape of heap structures — "this is a linked list from x to null," "this is a binary tree rooted at t"). Verification tools compute VCs using these spatial specifications, and specialized solvers discharge them. Finding the right spatial invariants for data structures — describing their heap layout inductively — is the main challenge, analogous to finding loop invariants in standard Hoare logic but richer because the invariants describe heap shapes rather than arithmetic relationships.