Separation Logic

Separation logic is a logic for reasoning about programs that manipulate heap-allocated memory, developed by John C. Reynolds in 2002 as an extension of Hoare logic. It is the formal foundation of modern program verification for systems with pointers, references, and dynamic memory allocation — the very systems that are most prone to the bugs that conventional type systems cannot catch: memory leaks, use-after-free, double-free, and null pointer dereferences.

The central insight of separation logic is the separating conjunction operator, written ∗. The assertion P ∗ Q means that the heap can be divided into two disjoint parts, one satisfying P and the other satisfying Q. This seemingly simple operator enables local reasoning: to verify a function, you need only consider the memory it touches, not the entire heap. The frame rule — if a command operates on a portion of the heap described by P, and the rest of the heap satisfies Q, then the command operates on the whole heap described by P ∗ Q — is the key theorem that makes this local reasoning sound.

Separation logic has been industrialized through tools like the Iris framework (built in Coq), the Verified Software Toolchain (VST), and Facebook's Infer static analyzer. Infer uses a variant of separation logic called bi-abduction to automatically infer memory safety properties of C and Java code, checking millions of lines of code at Facebook and finding thousands of bugs before they reach production. The logic that Reynolds developed as a mathematical abstraction has become a practical engineering tool, and its transition from theory to practice is one of the most successful stories in formal methods.

The connection to Type Theory is subtle and important. Separation logic is not a type system, but it plays a similar role: it is a formal discipline that prevents classes of error at the level of reasoning rather than at the level of execution. Where Dependent Types encode correctness properties in types, separation logic encodes them in assertions about the heap. The two approaches are complementary, and their combination — dependent types for functional correctness, separation logic for memory safety — is the frontier of verified systems programming.