Introduction

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}\{P\}\; C\; \{Q\} says: if precondition PP holds before command CC runs, postcondition QQ 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∗QP * Q. It asserts PP and QQ, but with a crucial extra: the heap regions they describe are disjoint. If PP talks about cell xx and QQ talks about cell yy, then x≠yx \neq y is guaranteed for free.

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

Heap Reasoning Demo

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.

<!-- Heap visualizer: address column, editable value column, owner badge, free button. -->
<div class="hint">Each row is a heap cell with an address and a value. Cells owned by <b>P</b>, <b>Q</b>, or <b>F</b> (frame) are automatically disjoint — that is the separating conjunction P ∗ Q ∗ F. Allocate cells, edit their values, then click <b>Apply frame rule</b> to see local reasoning in action.</div>
<div class="heap-area">
  <div class="heap-header">
    <span>Address</span>
    <span>Value</span>
    <span>Owned by</span>
    <span></span>
  </div>
  <div id="heap-rows"></div>
</div>
<div class="assertion-panel">
  <div class="assert-label">Current heap 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">Allocate cell</button>
  <button id="btn-frame" type="button">Apply frame rule</button>
  <button id="btn-reset" type="button" class="ghost">Reset</button>
</div>

/* Styles for the heap rows, owner badges, assertion panel, and controls. */
* { 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; }

const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Separation logic heap demo: each cell has an owner (P, Q, or F).
// The separating conjunction P * Q asserts P and Q hold on DISJOINT heap regions.
// The frame rule: {P} C {Q} => {P * F} C {Q * F} when C does not touch F.

// Owners cycle P -> Q -> F as cells are allocated, ensuring disjointness.
const OWNERS = ['P', 'Q', 'F'];
let heap = [];     // array of {addr, val, owner}
let nextAddr = 100; // starting hex address

// Allocate a new heap cell and assign the next owner.
function allocCell() {
  if (heap.length >= 6) { setStatus('Heap is full (6 cells max for this demo).', 'bad'); return; }
  const owner = OWNERS[heap.length % OWNERS.length];
  heap.push({ addr: nextAddr, val: 0, owner });
  nextAddr += 4;
  renderHeap();
  updateAssertion();
  setStatus(fmt('Allocated cell at address 0x%v%.', { v: nextAddr - 4 }), 'ok');
}

// Render all heap rows into the DOM.
function renderHeap() {
  const container = document.getElementById('heap-rows');
  container.innerHTML = '';
  heap.forEach((cell, idx) => {
    const row = document.createElement('div');
    row.className = 'heap-row fresh';
    // address column
    const addrSpan = document.createElement('span');
    addrSpan.className = 'addr';
    addrSpan.textContent = '0x' + cell.addr.toString(16).toUpperCase();
    // editable value column
    const valInput = document.createElement('input');
    valInput.type = 'number';
    valInput.className = 'val-input';
    valInput.value = cell.val;
    valInput.title = 'Edit cell value';
    valInput.addEventListener('change', () => {
      heap[idx].val = parseInt(valInput.value) || 0;
      updateAssertion();
    });
    // ownership badge column
    const ownerSpan = document.createElement('span');
    const badge = document.createElement('span');
    badge.className = 'owner-badge owner-' + cell.owner;
    badge.textContent = cell.owner;
    ownerSpan.appendChild(badge);
    // free button column
    const freeBtn = document.createElement('button');
    freeBtn.className = 'btn-free';
    freeBtn.textContent = 'Free';
    freeBtn.title = 'Free this cell';
    freeBtn.addEventListener('click', () => {
      heap.splice(idx, 1);
      renderHeap();
      updateAssertion();
      setStatus('Cell freed. Assertion updated.', 'ok');
    });
    row.append(addrSpan, valInput, ownerSpan, freeBtn);
    container.appendChild(row);
  });
}

// Build and display the current separation-logic assertion.
function updateAssertion() {
  const display = document.getElementById('assertion-display');
  if (heap.length === 0) {
    display.textContent = 'emp (empty heap)';
    display.className = 'assertion bad';
    return;
  }
  // Each cell contributes one points-to fact: addr |-> val [owner].
  const parts = heap.map(c => '0x' + c.addr.toString(16).toUpperCase() + ' ↦ ' + c.val + ' [' + c.owner + ']');
  // * is the separating conjunction (Unicode asterisk operator U+2217).
  display.textContent = parts.join(' ∗ ');
  display.className = 'assertion sep';
}

// Apply the frame rule: show that P and Q regions are disjoint, and F is untouched.
function applyFrame() {
  const pCells = heap.filter(c => c.owner === 'P');
  const qCells = heap.filter(c => c.owner === 'Q');
  const fCells = heap.filter(c => c.owner === 'F');
  if (pCells.length === 0 || qCells.length === 0) {
    setStatus('Allocate at least one P cell and one Q cell first.', 'bad');
    return;
  }
  // All addresses must be distinct (disjointness required by * operator).
  const addrs = heap.map(c => c.addr);
  const unique = new Set(addrs).size === addrs.length;
  if (!unique) { setStatus('Aliasing detected: two cells share an address!', 'bad'); return; }
  // Build human-readable representation of P, Q, and frame F parts.
  const pPart = pCells.map(c => '0x' + c.addr.toString(16).toUpperCase() + '↦' + c.val).join(' ∗ ');
  const qPart = qCells.map(c => '0x' + c.addr.toString(16).toUpperCase() + '↦' + c.val).join(' ∗ ');
  const fPart = fCells.length ? ' ∗ F₀(' + fCells.map(c => '0x' + c.addr.toString(16).toUpperCase()).join(',') + ')' : '';
  setStatus(fmt('Frame rule applied: {%pPart%} C {%qPart%}%fPart% — frame F unchanged.', { pPart: pPart, qPart: qPart, fPart: fPart }), 'ok');
}

function setStatus(t, cls) {
  const s = document.getElementById('status');
  s.textContent = t;
  s.className = 'status ' + cls;
}

// Wire up buttons and initialize the empty heap view.
document.getElementById('btn-alloc').addEventListener('click', allocCell);
document.getElementById('btn-frame').addEventListener('click', applyFrame);
document.getElementById('btn-reset').addEventListener('click', () => {
  heap = [];
  nextAddr = 100;
  renderHeap();
  updateAssertion();
  setStatus('', '');
});
renderHeap();
updateAssertion();
Result
Console

Notice: once you allocate two cells independently they are automatically disjoint — the separating conjunction P∗QP * 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∗QP * Q breaks, because the heap no longer contains both disjoint parts.

The Real Complexity

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 Σ10\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↦yx \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}\{P\}\; C\; \{Q\} and CC does not modify the free variables of FF, then {P∗F}  C  {Q∗F}\{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 FF.
  • 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.

Where It Matters

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 II attached to a lock ensures that whenever a thread holds the lock it also owns the heap cells guarded by II — 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.

Conclusion

Separation logic shows how a single well-chosen connective can transform an intractable problem. Aliasing made heap reasoning combinatorially explosive; the separating conjunction P∗QP * 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.

Share this article

Pick a channel — or use your device's native share sheet.

Comments

Loading comments...

https://www.kipuhub.com/en/article/separation-logic/Content licensed under CC BY-NC 4.0.