Introduction

A program, a hardware circuit, a network protocol — any of them can be described as a transition system: a set of states and rules that say how the system moves from one state to the next. A bug is just a bad state the system should never reach.

Bounded Model Checking (BMC) asks a sharply focused question: is there an execution of at most kk steps that lands in a bad state? The idea, introduced by Armin Biere, Alessandro Cimatti, Edmund Clarke, and Yunshan Zhu in 1999, is disarmingly simple — unroll the transition relation kk times, add a clause asserting that the bad state is reached at some step, and hand the whole formula to a SAT solver.

If the solver says satisfiable, the satisfying assignment is an exact bug trace: state at step 0, state at step 1, ..., state at step kk. If it says unsatisfiable, no bug exists within kk steps. Increase kk, repeat.

This one trick turned formal verification from a niche academic exercise into a tool that chip designers and software engineers use every day.

Try It

The demo below models a tiny traffic-light controller as a transition system. States are the light color; one transition is broken (it can skip straight to an illegal combination). Choose a bound kk and click Run BMC — the tool unrolls the system kk steps, builds the propositional formula, and searches for a path that hits the forbidden state.

<!-- BMC demo: traffic-light controller with one faulty transition -->
<div class="bmc-wrap">
  <div class="controls">
    <label for="bound-slider">Bound k = <strong id="bound-val">3</strong></label>
    <input type="range" id="bound-slider" min="1" max="8" value="3" />
    <button id="run-btn" type="button">Run BMC</button>
    <button id="reset-btn" type="button" class="ghost">Reset</button>
  </div>
  <div class="result-box" id="result-box">
    <span class="result-text" id="result-text">Choose a bound and click Run BMC.</span>
  </div>
  <div class="trace-area" id="trace-area"></div>
  <details class="formula-details">
    <summary>Show propositional formula</summary>
    <pre class="formula-pre" id="formula-pre"></pre>
  </details>
</div>

/* Bounded Model Checking demo — traffic-light styles */
* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; margin: 0; color: #222; }

.bmc-wrap { display: flex; flex-direction: column; gap: .8rem; }

/* control row */
.controls { display: flex; flex-wrap: wrap; align-items: center; gap: .6rem; }
label { font-size: .9rem; }
input[type=range] { flex: 1; min-width: 120px; }
button { font: 600 14px system-ui; padding: .4rem .85rem;
         border: 1px solid #1d3557; background: #1d3557; color: #fff;
         border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }

/* result banner */
.result-box { border-radius: 8px; padding: .5rem .9rem; font-weight: 600; font-size: .95rem;
              background: #e8eef3; border: 1px solid #cdd9e3; min-height: 2.4rem;
              display: flex; align-items: center; }
.result-box.ok   { background: #d4edda; border-color: #68b37c; color: #0a5c23; }
.result-box.fail { background: #f8d7da; border-color: #e27b85; color: #8b1c26; }

/* counterexample trace cards */
.trace-area { display: flex; flex-wrap: wrap; gap: .5rem; }
.step-card { border: 1px solid #cdd9e3; border-radius: 8px; padding: .5rem .7rem;
             min-width: 90px; text-align: center; background: #f4f7fa; }
.step-card.bad { background: #fde8ea; border-color: #e27b85; }
.step-card .step-label { font-size: .72rem; color: #666; margin-bottom: .2rem; }
.step-card .light-icon { font-size: 1.6rem; line-height: 1; }
.step-card .state-name { font-size: .78rem; font-weight: 600; margin-top: .15rem; }
.step-card .transition { font-size: .7rem; color: #555; margin-top: .18rem; }

/* formula display */
.formula-details { font-size: .82rem; }
.formula-details summary { cursor: pointer; color: #1d3557; font-weight: 600; margin-bottom: .3rem; }
.formula-pre { background: #f0f4f8; border: 1px solid #cdd9e3; border-radius: 6px;
               padding: .6rem .8rem; overflow-x: auto; white-space: pre-wrap; color: #333;
               font-size: .78rem; line-height: 1.5; }

const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Bounded Model Checking demo — traffic-light transition system
// System: 5 states, one faulty transition green->bug (red+green simultaneously).

// All states in the system
const STATES = ['red', 'red_yellow', 'green', 'yellow', 'bug'];
// Human-readable state labels
const STATE_LABEL = {
  red:        'Red',
  red_yellow: 'Red+Yellow',
  green:      'Green',
  yellow:     'Yellow',
  bug:        'Red+Green (BUG)'
};
const STATE_ICON = {
  red: '🔴', red_yellow: '🟡🔴', green: '🟢', yellow: '🟡', bug: '🔴🟢'
};
// Transition relation: maps each state to its successor states
// The faulty transition green->bug represents an illegal hardware state.
const TRANSITIONS = {
  red:        ['red_yellow'],
  red_yellow: ['green'],
  green:      ['yellow', 'bug'],
  yellow:     ['red'],
  bug:        []
};
const INIT_STATE = 'red';
const BAD_STATE  = 'bug';

// runBMC(k): BFS up to depth k looking for a path to BAD_STATE
// Returns the path if found, null if no counterexample within k steps.
function runBMC(k) {
  // BFS queue: each entry is the path taken so far
  const queue = [['red']];
  while (queue.length > 0) {
    const path = queue.shift();
    const last = path[path.length - 1];
    if (last === BAD_STATE) return path;
    if (path.length - 1 >= k) continue;
    for (const next of (TRANSITIONS[last] || [])) {
      queue.push([...path, next]);
    }
  }
  return null;
}

// buildFormulaText: display the propositional encoding for the current k
function buildFormulaText(k) {
  const lines = [];
  lines.push('Initial condition:');
  lines.push('  s_0 = red');
  lines.push('');
  lines.push('Transition constraints (for each i in 0..k-1):');
  for (const [src, dsts] of Object.entries(TRANSITIONS)) {
    if (dsts.length > 0) {
      lines.push('  s_i = ' + src + '  →  s_{i+1} ∈ {' + dsts.join(', ') + '}');
    }
  }
  lines.push('');
  lines.push('BMC query (find BAD within k steps):');
  lines.push('  s_0 = red  ∧  T(s_0,s_1)  ∧ ... ∧  T(s_{k-1},s_k)  ∧  (s_0=bug ∨ ... ∨ s_k=bug)');
  lines.push('');
  lines.push(fmt('Bound: k = %k%', { k: k }));
  lines.push(fmt('Variables: %k%%v% × |STATES| = %v2% boolean variables', { k: k, v: 1, v2: (k + 1) * STATES.length }));
  return lines.join('\n');
}

// renderTrace: show step-by-step counterexample cards
function renderTrace(path) {
  const area = document.getElementById('trace-area');
  area.innerHTML = '';
  path.forEach((state, i) => {
    const card = document.createElement('div');
    const isBad = state === BAD_STATE;
    card.className = 'step-card' + (isBad ? ' bad' : '');

    const stepLabel = document.createElement('div');
    stepLabel.className = 'step-label';
    stepLabel.textContent = fmt('Step %i%', { i: i });
    card.appendChild(stepLabel);

    const icon = document.createElement('div');
    icon.className = 'light-icon';
    icon.textContent = STATE_ICON[state] || '?';
    card.appendChild(icon);

    const name = document.createElement('div');
    name.className = 'state-name';
    name.textContent = STATE_LABEL[state] || state;
    card.appendChild(name);

    if (i < path.length - 1) {
      const arrow = document.createElement('div');
      arrow.className = 'transition';
      arrow.textContent = '↓';
      card.appendChild(arrow);
    }
    if (isBad) {
      const flag = document.createElement('div');
      flag.className = 'transition';
      flag.textContent = '⚠ BUG STATE';
      card.appendChild(flag);
    }
    area.appendChild(card);
  });
}

function run() {
  const k = parseInt(document.getElementById('bound-slider').value, 10);
  const box = document.getElementById('result-box');
  const txt = document.getElementById('result-text');
  const area = document.getElementById('trace-area');
  const pre  = document.getElementById('formula-pre');

  pre.textContent = buildFormulaText(k);

  const trace = runBMC(k);
  if (trace) {
    box.className = 'result-box fail';
    txt.textContent = fmt('Counterexample found at step %v% — see trace below.', { v: trace.length - 1 });
    renderTrace(trace);
    console.log('BMC counterexample trace:', trace.join(' → '));
  } else {
    box.className = 'result-box ok';
    txt.textContent = fmt('No counterexample within k = %k% steps. Try a larger bound.', { k: k });
    area.innerHTML = '';
    console.log('BMC result: no bug within k =', k);
  }
}

document.getElementById('run-btn').addEventListener('click', run);
document.getElementById('reset-btn').addEventListener('click', () => {
  document.getElementById('bound-slider').value = 3;
  document.getElementById('bound-val').textContent = '3';
  document.getElementById('result-box').className = 'result-box';
  document.getElementById('result-text').textContent = 'Choose a bound and click Run BMC.';
  document.getElementById('trace-area').innerHTML = '';
  document.getElementById('formula-pre').textContent = '';
  console.log('Demo reset.');
});
document.getElementById('bound-slider').addEventListener('input', function () {
  document.getElementById('bound-val').textContent = this.value;
});
Result
Console

Notice what you see: when kk is too small the bug is out of reach and the result is no counterexample up to kk. Once kk is large enough the solver finds the exact step-by-step trace. This is the core promise of BMC — a concrete witness you can read and reproduce, not just a "bug exists" verdict.

The Real Complexity

Each BMC query is a SAT instance — and SAT is NP-complete. So finding a bug trace of length kk is NP-complete. That sounds alarming, but in practice modern SAT solvers handle formulas with millions of variables efficiently by exploiting structure, making BMC remarkably fast on real systems.

The formula for bound kk has size O(k⋅∣T∣)O(k \cdot |T|), where ∣T∣|T| is the size of one unrolled transition step. Each new unrolling adds one fresh copy of the transition variables, so the formula grows linearly with kk.

The incompleteness caveat. A "no counterexample up to kk" answer does not prove the system is correct — the bug might require more than kk steps. Two ways to get completeness:

  • Completeness threshold: for finite-state systems there exists a bound k∗k^* beyond which, if no bug exists, no new behavior can appear. Computing k∗k^* is hard in general, but it can sometimes be bounded using the diameter of the state graph.
  • Induction (k-induction): pair BMC with an inductive argument — if no bug in kk steps AND every kk-step sequence without a bug extends safely, then there is no bug at all. This is related to program equivalence and invariant checking.

The key insight: BMC trades completeness for speed and concrete witnesses. For bug-finding — the dominant use case — the incompleteness is acceptable because you stop as soon as the solver finds the trace.

Where It Matters

BMC has spread well beyond its academic birthplace into every domain where correctness matters:

  • Hardware verification: Intel, AMD, and others routinely apply BMC to gate-level netlists to catch timing violations and unreachable states before tape-out. Missing a bug at this stage can cost millions of dollars.
  • Software model checking: tools like CBMC (C Bounded Model Checker) unroll C programs into SAT/SMT formulas and find buffer overflows, null dereferences, and assertion violations — bugs that may hide for years in testing.
  • Security protocols: BMC can check whether an attacker with bounded resources can break a cryptographic handshake or forge a message within kk protocol steps.
  • Autonomous systems: verifying that a control loop never violates a safety invariant within the planning horizon is a BMC query at heart.
  • Teaching formal methods: because the reduction to SAT is explicit and mechanical, BMC is one of the clearest ways to show students what P vs NP has to do with the real world.

The formula pipeline — system →\to propositional logic →\to SAT solver →\to counterexample or "clean up to kk" — is now a standard component of industrial verification flows.

Conclusion

Bounded Model Checking distills a deep idea into a single move: any reachability question about a finite-state system is a satisfiability question in disguise. Unroll kk steps, assert the bad event, ask the solver. The answer is either a concrete bug you can hold in your hand or a proof that the bug cannot happen within the horizon.

The technique is incomplete — bounded horizons are not proofs of correctness — but in the real world that is often exactly the right trade-off. Hardware vendors ship chips with fewer errata. Software teams catch memory errors before they reach users. And every SAT breakthrough since 1999 has automatically made BMC faster.

The next time a safety-critical piece of software proves it has no buffer overflow, there is a good chance a SAT solver quietly verified it by pretending to be a time-traveler — checking every possible execution up to kk steps at once.

Share this article

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

Comments

Loading comments...

https://www.kipuhub.com/en/article/bounded-model-checking/Content licensed under CC BY-NC 4.0.