Separation Logic

Writing correct pointer programs is notoriously hard. Swap two nodes in a linked list, free a buffer, or pass a pointer into a helper — and somewhere, something you were not thinking about breaks. The culprit is almost always aliasing: two names pointing at the same memory cell, so changing one secretly changes the other.

Classical Hoare logic (the basis of most formal program verification) treats the memory as a single flat heap. A triple $\{P\}\; C\; \{Q\}$ says: if precondition $P$ holds before command $C$ runs, postcondition $Q$ holds after. That is clean and powerful — until aliasing forces you to carry every live pointer in every precondition just to rule out unexpected interactions. For large programs the bookkeeping explodes.

In 2001, John C. Reynolds and Peter O'Hearn introduced separation logic, which extends Hoare logic with one new connective: the separating conjunction $P * Q$. It asserts $P$ and $Q$, but with a crucial extra: the heap regions they describe are disjoint. If $P$ talks about cell $x$ and $Q$ talks about cell $y$, then $x \neq y$ is guaranteed for free.

From that one operator flows the frame rule, the cornerstone of local reasoning: if a command $C$ modifies only the cells mentioned in $P$, you can add any independent frame $F$ and the rule tells you the result without re-proving anything about $F$. That is the key insight that makes separation logic scale to real-world verifiers like Facebook Infer and VeriFast.

Below is a small heap visualizer. Each cell has an address and a value. Use the controls to allocate cells, write to them, and check separation assertions.

<!-- {{c_html_intro}} -->
<div class="hint">{{hint_para}}</div>
<div class="heap-area">
  <div class="heap-header">
    <span>{{label_addr}}</span>
    <span>{{label_val}}</span>
    <span>{{label_owns}}</span>
    <span></span>
  </div>
  <div id="heap-rows"></div>
</div>
<div class="assertion-panel">
  <div class="assert-label">{{label_assertion}}</div>
  <div id="assertion-display" class="assertion"></div>
</div>
<div class="status" id="status"></div>
<div class="btns">
  <button id="btn-alloc" type="button">{{btn_alloc}}</button>
  <button id="btn-frame" type="button">{{btn_frame}}</button>
  <button id="btn-reset" type="button" class="ghost">{{btn_reset}}</button>
</div>

/* {{c_css_intro}} */
* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; }
.hint { font-size: .88rem; color: #444; margin: 0 0 .8rem; line-height: 1.5; }
.heap-area { border: 1px solid #cdd9e3; border-radius: 8px; overflow: hidden; margin-bottom: .6rem; }
.heap-header { display: grid; grid-template-columns: 70px 1fr 1fr 80px;
               gap: 0; background: #d6e4ee; font: 600 .78rem system-ui; color: #1d3557; padding: .35rem .7rem; }
.heap-row { display: grid; grid-template-columns: 70px 1fr 1fr 80px;
            gap: 0; padding: .3rem .7rem; border-top: 1px solid #e8eef3;
            align-items: center; font: .85rem ui-monospace, monospace; }
.heap-row.fresh { animation: pop .25s ease; }
@keyframes pop { from { background: #cff4d2; } to { background: transparent; } }
.addr { color: #1d3557; font-weight: 700; }
.val-input { width: 70px; font: inherit; border: 1px solid #adb1b8; border-radius: 5px;
             padding: .15rem .35rem; background: #f4f7fa; }
.owner-badge { font-size: .78rem; padding: .1rem .5rem; border-radius: 12px; display: inline-block; }
.owner-P { background: #dbeafe; color: #1d4ed8; }
.owner-Q { background: #fde8cc; color: #b45309; }
.owner-F { background: #e0e7ff; color: #4338ca; }
.btn-free { font: 600 .75rem system-ui; padding: .15rem .5rem; border: 1px solid #c92f3c;
            background: #fff; color: #c92f3c; border-radius: 5px; cursor: pointer; }
.assertion-panel { background: #f4f7fa; border-radius: 8px; padding: .5rem .8rem; margin-bottom: .5rem; }
.assert-label { font: 600 .78rem system-ui; color: #555; margin-bottom: .25rem; }
.assertion { font: .88rem ui-monospace, monospace; color: #1d3557; min-height: 1.4em; word-break: break-all; }
.assertion.sep { color: #0a7d33; }
.assertion.bad { color: #c92f3c; }
.status { font-size: .95rem; font-weight: 600; margin: .4rem 0; min-height: 1.4em; }
.status.ok { color: #0a7d33; }
.status.bad { color: #c92f3c; }
.btns { display: flex; gap: .5rem; flex-wrap: wrap; }
button { font: 600 14px system-ui; padding: .45rem .9rem; border: 1px solid #1d3557;
         background: #1d3557; color: #fff; border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }

// Code not found

Notice: once you allocate two cells independently they are automatically disjoint — the separating conjunction $P * Q$ holds. Try writing a value to one cell and observe that the other cell's specification is untouched — that is the frame rule at work. Deallocate a cell and the assertion $P * Q$ breaks, because the heap no longer contains both disjoint parts.

Separation logic is more expressive than classical Hoare logic — and that power has a price.

• Full separation logic is undecidable. The validity problem — does a formula hold on every heap? — is $\Sigma_1^0$-complete when you combine the full first-order language with the separating conjunction. This is not surprising: even first-order arithmetic is undecidable.
• Useful fragments are decidable. The symbolic-heap fragment — used by most automated tools — restricts formulas to conjunctions of points-to facts ($x \mapsto y$) and equalities. Entailment in this fragment is in PSPACE, and many practical subsets are polynomial.
• The frame rule keeps reasoning local. The rule says: if $\{P\}\; C\; \{Q\}$ and $C$ does not modify the free variables of $F$, then $\{P * F\}\; C\; \{Q * F\}$. This means a proof about a small subroutine automatically lifts to any larger context — you never re-verify the unchanged frame $F$.
• Bi-abduction makes inference automatic. Facebook's Infer tool uses bi-abduction (Calcagno et al., 2011): given a call site, the tool infers both the missing precondition (what the callee needs) and the antiframe (what the caller still owns). This turns separation logic into a fully automatic interprocedural analysis.

The result is a sweet spot: the logic is undecidable in full generality, but the decidable fragment covers most real-world heap patterns, and the frame rule keeps the proof size manageable as programs grow.

Separation logic moved from theory to industry faster than almost any other formal-methods idea:

• Facebook / Meta Infer: deployed at scale since ~2015, Infer runs on every code change to iOS and Android apps. It uses bi-abduction on symbolic heaps to catch null-dereferences, memory leaks, and use-after-free bugs automatically, without annotations.
• VeriFast: an interactive verifier for C and Java that lets programmers write separation-logic specs as annotations and verifies them at compile time, catching buffer overflows and aliasing errors before they reach production.
• Concurrent separation logic: O'Hearn extended the logic to handle threads sharing a heap. A resource invariant $I$ attached to a lock ensures that whenever a thread holds the lock it also owns the heap cells guarded by $I$ — a clean formal account of the mutual-exclusion pattern. This was recognized with the ACM Turing Award to O'Hearn in 2023.
• Operating-system kernels: projects like seL4 and CertiKOS use separation-logic-based reasoning to verify that kernel data structures are not corrupted by concurrent operations.
• Rust's ownership types: while not literally separation logic, Rust's borrow checker enforces the same disjointness invariant at the type-system level, preventing data races and dangling pointers by construction.

Understand separation logic and you understand why Rust's borrow checker is sound, why Infer can analyze millions of lines without annotations, and how program synthesis tools prove generated code correct.

Separation logic shows how a single well-chosen connective can transform an intractable problem. Aliasing made heap reasoning combinatorially explosive; the separating conjunction $P * Q$ cuts through that by guaranteeing disjointness at the level of the logic itself. Every proof automatically knows which parts of memory it does not touch — and that is the insight the frame rule turns into scalable, compositional verification.

The logic is undecidable in full generality, but its decidable fragments cover the heap patterns that actually appear in programs. Facebook's Infer finds real bugs in real code every day using nothing more than symbolic heaps and bi-abduction. And Rust embeds the same disjointness discipline into the type system, making safe concurrency the default.

Sometimes the deepest theoretical insight and the most practical engineering fix are the same idea — just wearing different clothes. Separation logic is one of the clearest examples of that in all of computer science.