Introduction

Every chip that ships, every safety-critical controller that runs, rests on a question: can the system ever reach a bad state? Formal verification tools try to answer "no" with a mathematical proof. For decades, the dominant approach was bounded model checking — unroll the system step by step and ask a SAT solver "is a bad state reachable in kk steps?" It works, but answering "never" requires k→∞k \to \infty, which is expensive.

In 2011, Aaron R. Bradley published a radically different idea: IC3 (Incremental Construction of Inductive Clauses for Indubitable Correctness), also called PDR (Property-Directed Reachability). Instead of unrolling time, IC3 builds a sequence of frames — each a set of clauses over the state variables — and incrementally pushes blocking clauses forward until one frame becomes an inductive invariant: a set of states that cannot reach the bad property and is closed under the transition relation.

The key insight is laziness: IC3 only reasons about states that are one step away from the bad property, blocking them with clauses and then checking whether those clauses can be pushed earlier in the frame sequence. When two adjacent frames become equal, the algorithm has found a proof — without ever constructing the full reachable set.

Try It: Block the Bad States

The demo below shows a tiny transition system with four states. The red state is bad; the green state is the initial state. IC3 maintains a sequence of frames F0,F1,F2,…F_0, F_1, F_2, \dots; each frame is a set of states that are not yet known to reach bad.

<!-- IC3/PDR demo: transition system graph + frame list -->
<div class="layout">
  <div class="graph-panel">
    <h3 class="panel-title">Transition System</h3>
    <svg id="graph" viewBox="0 0 340 240" width="340" height="240" aria-label="Transition system graph with states S0 to S3"></svg>
  </div>
  <div class="frames-panel">
    <h3 class="panel-title">IC3 Frames</h3>
    <div id="frames-list" class="frames-list"></div>
  </div>
</div>
<div class="log-area">
  <div id="log" class="log"></div>
</div>
<div class="btns">
  <button id="step" type="button">Step</button>
  <button id="reset" type="button" class="ghost">Reset</button>
</div>
<div id="status" class="status"></div>

/* IC3/PDR demo styles */
* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; margin: 0; color: #222; }
.layout { display: flex; gap: 1rem; align-items: flex-start; flex-wrap: wrap; }
.graph-panel, .frames-panel { flex: 1 1 160px; }
.panel-title { font-size: .85rem; font-weight: 700; margin: 0 0 .4rem; color: #1d3557; text-transform: uppercase; letter-spacing: .04em; }
svg { display: block; border: 1px solid #dde3ea; border-radius: 10px; background: #f8fafc; }
.frames-list { display: flex; flex-direction: column; gap: .35rem; }
.frame-row { font-size: .82rem; padding: .3rem .5rem; border-radius: 6px; background: #eef2f7; border-left: 3px solid #1d3557; }
.frame-row.inductive { border-left-color: #0a7d33; background: #e8f7ed; }
.log-area { margin: .6rem 0 .4rem; max-height: 90px; overflow-y: auto; border: 1px solid #dde3ea; border-radius: 8px; background: #f8fafc; padding: .35rem .6rem; }
.log { font-size: .78rem; color: #444; line-height: 1.55; }
.log .entry { border-bottom: 1px solid #eee; padding: .15rem 0; }
.btns { display: flex; gap: .5rem; flex-wrap: wrap; margin-bottom: .4rem; }
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; }
button:disabled { opacity: .4; cursor: default; }
.status { font-size: 1rem; font-weight: 600; min-height: 1.4em; }
.status.ok { color: #0a7d33; }
.status.bad { color: #c92f3c; }
/* Node color classes applied via JS fill attribute */
.node-circle { stroke-width: 2; }
.node-label { font: 700 13px ui-monospace, monospace; }

const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// IC3 / Property-Directed Reachability demo.
// States: S0 (initial, green), S1, S2, S3 (bad, red).
// IC3 builds frames F0..Fn, blocking predecessors of bad and pushing clauses forward.

// All states in the system
// S0=initial, S1=intermediate, S2=loop, S3=bad
const STATES = ['S0','S1','S2','S3'];
const INIT = 'S0';       // initial state
const BAD  = 'S3';       // bad (unsafe) state
// Transition relation: TRANS[s] = list of successors of s
const TRANS = { S0:['S1','S2'], S1:['S2'], S2:['S1'], S3:['S3'] };

// SVG positions for each state node
const POS = { S0:[60,120], S1:[160,50], S2:[160,190], S3:[280,120] };

// Node fill colors
const COLOR = {
  default:'#c9ccd1', init:'#2ecc71', bad:'#e63946',
  blocked:'#f0a500', inductive:'#1d3557'
};

// IC3 frames: frames[i] is the set of states not yet known to reach bad in i steps
// Initially every frame holds all states; we progressively remove states.
// F0 = {S0,S1,S2,S3} (all states).  Each step blocks predecessors of bad.
let frames = [];   // frames[i] = Set of states still in frame i
let obligations = []; // Stack of (frame, state) pairs that need to be blocked
let done = false;

function allStates(){ return new Set(STATES); }

function predecessors(stateSet){
  // Return all states that can reach any state in stateSet in one step
  const preds = new Set();
  for(const s of STATES){
    if(TRANS[s].some(t => stateSet.has(t))) preds.add(s);
  }
  return preds;
}

function intersect(a,b){ return new Set([...a].filter(x=>b.has(x))); }
function setMinus(a,b){ return new Set([...a].filter(x=>!b.has(x))); }
function setsEqual(a,b){ return a.size===b.size && [...a].every(x=>b.has(x)); }

function initIC3(){
  // Initialize IC3: two frames, seed obligations from predecessors of BAD
  frames = [allStates(), allStates()]; // F0 and F1 start as all states
  obligations = [];
  // Seed: block predecessors of BAD from F1
  const predBad = predecessors(new Set([BAD]));
  const toBlock = intersect(predBad, frames[1]);
  for(const s of toBlock) obligations.push({frame:1, state:s});
  done = false;
}

function logEntry(msg){
  const d = document.getElementById('log');
  const e = document.createElement('div'); e.className='entry'; e.textContent=msg;
  d.appendChild(e); d.scrollTop=d.scrollHeight;
}

function renderGraph(){
  const svg = document.getElementById('graph');
  svg.innerHTML = '';
  // Draw transition arrows
  for(const s of STATES){
    for(const t of TRANS[s]){
      const [x1,y1]=POS[s]; const [x2,y2]=POS[t];
      const dx=x2-x1,dy=y2-y1,len=Math.sqrt(dx*dx+dy*dy); if(len===0)continue;
      const ux=dx/len,uy=dy/len,r=22;
      const sx=x1+ux*r,sy=y1+uy*r,ex=x2-ux*r,ey=y2-uy*r;
      const line=document.createElementNS('http://www.w3.org/2000/svg','line');
      line.setAttribute('x1',sx);line.setAttribute('y1',sy);
      line.setAttribute('x2',ex);line.setAttribute('y2',ey);
      line.setAttribute('stroke','#aab3bf');line.setAttribute('stroke-width','1.8');
      line.setAttribute('marker-end','url(#arr)'); svg.appendChild(line);
    }
  }
  // Draw state nodes
  for(const s of STATES){
    const [cx,cy]=POS[s];
    // Pick fill color: init=green, bad=red, blocked=orange, default=gray
    let fill = COLOR.default;
    if(s===INIT) fill=COLOR.init;
    if(s===BAD)  fill=COLOR.bad;
    const lastFrame = frames[frames.length-1];
    if(lastFrame && !lastFrame.has(s) && s!==INIT && s!==BAD) fill=COLOR.blocked;

    const circle=document.createElementNS('http://www.w3.org/2000/svg','circle');
    circle.setAttribute('cx',cx);circle.setAttribute('cy',cy);circle.setAttribute('r',22);
    circle.setAttribute('fill',fill);circle.setAttribute('stroke','#fff');
    circle.setAttribute('stroke-width','2');circle.setAttribute('class','node-circle');
    svg.appendChild(circle);

    const text=document.createElementNS('http://www.w3.org/2000/svg','text');
    text.setAttribute('x',cx);text.setAttribute('y',cy+5);
    text.setAttribute('text-anchor','middle');text.setAttribute('fill','#fff');
    text.setAttribute('class','node-label');text.textContent=s;
    svg.appendChild(text);
  }
  // Arrowhead marker definition (prepend so arrows render on top)
  const defs=document.createElementNS('http://www.w3.org/2000/svg','defs');
  const marker=document.createElementNS('http://www.w3.org/2000/svg','marker');
  marker.setAttribute('id','arr');marker.setAttribute('markerWidth','8');
  marker.setAttribute('markerHeight','6');marker.setAttribute('refX','6');
  marker.setAttribute('refY','3');marker.setAttribute('orient','auto');
  const poly=document.createElementNS('http://www.w3.org/2000/svg','polygon');
  poly.setAttribute('points','0 0, 8 3, 0 6');poly.setAttribute('fill','#aab3bf');
  marker.appendChild(poly);defs.appendChild(marker);svg.insertBefore(defs,svg.firstChild);
}

function renderFrames(){
  const el = document.getElementById('frames-list');
  el.innerHTML = '';
  frames.forEach((f,i)=>{
    const div=document.createElement('div');
    const isInd = i>0 && setsEqual(frames[i],frames[i-1]);
    div.className = 'frame-row' + (isInd?' inductive':'');
    const stateList = [...f].join(', ') || '∅';
    div.textContent = 'F'+i+': {'+stateList+'}' + (isInd ? ' ✓' : '');
    el.appendChild(div);
  });
}

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

function step(){
  if(done){ setStatus(`Already proved — reset to start over.`,'ok'); return; }

  if(obligations.length===0){
    // No obligations left: try to push blocked states to earlier frames
    // A state blocked in frame i can be removed from frame i+1 if it stays blocked
    let pushed = false;
    for(let i=1;i<frames.length-1;i++){
      const fi=frames[i], fi1=frames[i+1];
      // States not in frame i are blocked; remove them from i+1 if present
      const blocked = setMinus(allStates(), fi);
      for(const s of blocked){
        if(fi1.has(s)){
          fi1.delete(s);
          logEntry(fmt(`Pushed block of %s% from F%i% to F%i%%v%.`, { s: s, i: i, v: 1 }));
          pushed=true;
        }
      }
    }
    // Check if any two adjacent frames are equal (inductive invariant found)
    for(let i=1;i<frames.length;i++){
      if(setsEqual(frames[i],frames[i-1])){
        done=true;
        logEntry(fmt(`Frame F%i% == frame F%v% — inductive invariant found. Safety proved!`, { i: i, v: i-1 }));
        setStatus(`Safety proved! An inductive invariant was found.`,'ok');
        document.getElementById('step').disabled=true;
        renderFrames(); renderGraph(); return;
      }
    }
    // No invariant yet: add a new frame and seed new obligations
    frames.push(new Set(frames[frames.length-1]));
    logEntry(fmt(`Extended to new frame F%v%.`, { v: frames.length-1 }));
    const predBad=predecessors(new Set([BAD]));
    const toBlock=intersect(predBad,frames[frames.length-1]);
    for(const s of toBlock) obligations.push({frame:frames.length-1,state:s});
    renderFrames(); renderGraph();
    setStatus(fmt(`Added frame F%v%. New obligations seeded.`, { v: frames.length-1 }),'');
    return;
  }

  // Process next obligation: block the state from the given frame
  const {frame,state} = obligations.pop();
  // Already removed from this frame; nothing to do
  if(!frames[frame].has(state)){
    logEntry(fmt(`State %state% already blocked in frame F%frame%.`, { state: state, frame: frame }));
    renderFrames(); renderGraph();
    return;
  }
  // Block: remove state from this frame
  frames[frame].delete(state);
  logEntry(fmt(`Blocked state %state% from frame F%frame%.`, { state: state, frame: frame }));

  // Propagate backwards: predecessors of blocked state also need blocking in earlier frame
  if(frame>1){
    const preds=predecessors(new Set([state]));
    const toBlock=intersect(preds,frames[frame-1]);
    for(const s of toBlock){
      obligations.push({frame:frame-1,state:s});
    }
    if(toBlock.size>0){
      logEntry(fmt(`Propagating obligation to frame F%v%.`, { v: frame-1 }));
    }
  }
  renderFrames(); renderGraph();
  setStatus(fmt(`Blocked state %state% from frame F%frame%.`, { state: state, frame: frame }),'');
}

document.getElementById('step').addEventListener('click',step);
document.getElementById('reset').addEventListener('click',()=>{
  initIC3();
  document.getElementById('log').innerHTML='';
  document.getElementById('step').disabled=false;
  renderFrames(); renderGraph();
  setStatus(`Reset. Click Step to run IC3.`,'');
});

initIC3();
renderFrames();
renderGraph();
setStatus(`Click Step to run IC3 step by step.`,'');
Result
Console

Click Step to let IC3 process one obligation: it picks the highest frame with a predecessor of bad, tries to block that predecessor, and pushes the blocking clause forward. When two consecutive frames hold the same set of states, the algorithm has found an inductive invariant and terminates with a safety proof. Click Reset to start over.

The Real Complexity

How hard is the safety problem that IC3 solves?

  • The problem itself is PSPACE-complete for general finite-state systems: deciding whether a bad state is reachable is as hard as any alternating polynomial-space computation.
  • IC3 is sound and complete: if the property holds, IC3 will eventually find an inductive invariant and terminate; if the property fails, IC3 will produce a counterexample trace.
  • Each SAT call is polynomial-time (assuming P≠NP\text{P} \neq \text{NP}, it is exponential worst-case, but in practice SAT solvers handle industrial instances in seconds). IC3 makes O(n2)O(n^2) SAT calls where nn is the length of the shortest counterexample or invariant, so the total work is polynomial in nn — which is exponentially better than explicit-state enumeration.
  • No unrolling needed: unlike bounded model checking, IC3 never creates a formula of size O(k⋅∣T∣)O(k \cdot |T|) where kk is the bound. It reasons about two consecutive time steps at a time.
  • Compared to BDDs: Binary Decision Diagram-based model checkers can blow up in memory for wide state spaces. IC3's clause-based representation scales far better on industrial hardware.

The algorithm sits at a sweet spot: it is complete (unlike pure BMC), memory-efficient (unlike BDDs), and fast in practice (unlike explicit-state enumeration). It is now the engine inside most industrial hardware model checkers, including those used by major semiconductor companies.

A related idea is k-induction: instead of single-step induction, check that no bad state is reachable in kk steps and that any kk-step path to bad is blocked. IC3 subsumes kk-induction by building the necessary kk automatically as its frame sequence grows.

Where It Matters

IC3/PDR changed what is possible in formal verification. Today it powers:

  • Hardware design verification: every major chip vendor runs PDR-based tools to prove that bus protocols, memory controllers and CPU pipelines cannot reach forbidden states. ARM, Intel and RISC-V implementations rely on it.
  • Software model checking: tools like SeaHorn and Spacer lift IC3 to programs via the theory of linear arithmetic and uninterpreted functions, proving absence of null-pointer dereferences or buffer overflows.
  • Security protocol analysis: IC3 can prove that an attacker can never reach a state where a secret is leaked, even under all possible message interleavings.
  • Concurrency verification: combined with abstraction-refinement, IC3 handles concurrent systems where explicit state enumeration is completely infeasible.

The insight — block bad states lazily, push clauses forward, stop when a frame is inductive — is general enough that researchers have extended it to probabilistic systems, timed automata, and even infinite-state programs via abstraction.

IC3's success also revitalized interest in SAT as a model-checking engine. While early model checkers used BDDs, IC3 showed that a well-structured sequence of SAT queries can outperform symbolic methods by several orders of magnitude on the hardware benchmarks that matter in industry.

Conclusion

IC3/PDR is a masterclass in algorithmic ingenuity: instead of asking "can bad be reached in kk steps?" for growing kk, it asks "what states can I prove are not on any path to bad?" and builds that answer incrementally. The result is an algorithm that is complete, memory-efficient, and fast enough to verify chips with millions of state bits.

The deeper lesson is about the power of inductive reasoning in verification. Proving that a property holds forever is hard in general — but if you can find a set of states that is both reachable from the initial state and closed under transitions, you have an invariant that certifies safety for all time, not just for the first kk steps.

Next time you trust a CPU or a network protocol, know that somewhere an IC3 engine ran, built its frames, pushed its clauses forward, and quietly declared: no bad state is reachable. That guarantee is harder to give — and harder to explain — than almost anything in P vs NP.

Share this article

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

Comments

Loading comments...

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