Model Checking — Senior Level¶

Roadmap: Formal Methods & Verification → Model Checking The middle page taught you that a model checker explores every reachable state and hands you a counterexample. This page is about the machinery underneath: how ¬φ becomes a Büchi automaton, why a lasso is a liveness bug, how a SAT solver finds a 40-step deadlock without ever enumerating states, and why the hardest problem in the field is not the algorithm but the gap between your model and the system it claims to describe.

Table of Contents¶

1. Introduction
2. Prerequisites
3. Glossary
4. Core Concept 1 — Explicit-State Reachability and the Visited Set
5. Core Concept 2 — The Automata-Theoretic Approach to LTL
6. Core Concept 3 — Nested DFS, Accepting Cycles, and the Lasso
7. Core Concept 4 — State Hashing and Bitstate Supertrace
8. Core Concept 5 — Symbolic Model Checking with BDDs
9. Core Concept 6 — Bounded Model Checking with SAT/SMT
10. Core Concept 7 — From Bounded to Complete: k-Induction and IC3/PDR
11. Core Concept 8 — Predicate Abstraction and CEGAR
12. Core Concept 9 — Fighting the Explosion: POR, Symmetry, Compositional
13. Core Concept 10 — Software Model Checking in Practice
14. Core Concept 11 — Liveness and Fairness in the Automata Framework
15. Real-World Examples
16. Mental Models
17. Common Mistakes
18. Test Yourself
19. Cheat Sheet
20. Summary
21. Further Reading
22. Related Topics

Introduction¶

Focus: The algorithms that make exhaustive verification tractable, and the discipline that keeps it honest.

By the middle level you can run SPIN or TLC, write an assert and an LTL property, read a counterexample trace, and explain why state explosion is the central enemy. You can use a model checker. The senior jump is understanding how it works underneath — because that is what lets you choose the right engine, diagnose why a check ran out of memory at 10⁹ states, decide whether bitstate hashing's coverage estimate is good enough to ship on, and recognise when a "verified" model is verifying the wrong thing.

There are three families of model-checking technology, and they are not interchangeable. Explicit-state checkers (SPIN, TLC) enumerate concrete states into a hash table and excel at concurrency and liveness. Symbolic checkers (the SMV lineage) manipulate sets of states as Boolean formulas via BDDs and conquer control-heavy hardware. SAT/SMT-based checkers (CBMC, modern IC3/PDR engines) encode the problem as a satisfiability query and are the most effective bug-finders ever built for software. Each rests on a different core algorithm — nested DFS over a product automaton, fixpoint iteration over BDDs, unrolling into a SAT formula — and a senior reasons fluently across all three. This page is those algorithms, and the limits that no algorithm removes.

Prerequisites¶

• Required: You've internalized middle.md — Kripke structures, reachability, safety vs liveness, LTL/CTL basics, state explosion, reading a counterexample.
• Required: Comfort with graph search (DFS/BFS), the notion of a fixpoint, and propositional logic / CNF.
• Helpful: You've written a non-trivial SPIN (Promela) or TLA+ spec and watched it blow up on memory.
• Helpful: A working memory of automata theory — NFA/DFA, ω-words, what "accepting" means on an infinite run.
• Helpful: You know what a SAT solver and an SMT solver do, at least as black boxes (DPLL/CDCL, theories of arithmetic and arrays).

Glossary¶

Core Concept 1 — Explicit-State Reachability and the Visited Set¶

Strip a model checker to its core and, for safety properties (something bad never happens — an assertion, an invariant, a deadlock), it is a graph search with one extra data structure:

ExplicitSafetyCheck(initial, transitions, bad):
    Visited = HashSet()           # the dominant memory cost of the whole field
    Stack   = [initial]           # DFS; a Queue gives BFS (shortest counterexample)
    while Stack not empty:
        s = Stack.pop()
        if s in bad: return COUNTEREXAMPLE(path_to(s))
        if s in Visited: continue
        Visited.add(s)
        for s' in transitions(s):
            Stack.push(s')
    return SAFE                    # the whole reachable set was explored, bad unreachable

Two design choices in those eight lines decide everything. DFS vs BFS: DFS uses memory proportional to path depth and finds a counterexample fast; BFS uses memory proportional to a frontier but finds the shortest counterexample — which matters enormously, because a 6-step trace is debuggable and a 600-step trace is not. SPIN defaults to DFS (memory-frugal, deep models); TLC does a BFS-like layered exploration precisely to give you minimal counterexamples.

The second choice is the Visited set itself. It is what makes the search terminate on a model with cycles and what makes it exhaustive rather than a random walk. It is also where all the memory goes: a real spec has states of dozens to hundreds of bytes, and 10⁸ states is routine. Every serious explicit-state optimization — state compression, hashing, the supertrace trick of Concept 4 — is ultimately an attack on the size of Visited.

Key insight: A safety model checker is BFS/DFS with a visited set. Everything sophisticated in the explicit-state world is either (a) a cheaper way to store Visited, or (b) a way to visit fewer states without losing soundness. Hold that frame and the rest of the field organizes itself.

This handles safety. Liveness — "the system eventually responds," "no process starves" — cannot be reduced to "is a bad state reachable," because the violation is not a state but an infinite behaviour: a run that loops forever without ever responding. For that we need automata over infinite words.

Core Concept 2 — The Automata-Theoretic Approach to LTL¶

This is the intellectual heart of explicit-state liveness checking, and the single most worthwhile idea to internalize at the senior level. The framework (Vardi–Wolper) reduces "does the system satisfy φ?" to a question about automata over infinite words.

The pipeline:

1. Model the system as a Büchi automaton A_sys. A run of the system is an infinite sequence of states; the system's language L(A_sys) is the set of all its infinite behaviours.
2. Negate the property and translate ¬φ into a Büchi automaton A_¬φ whose language is exactly the behaviours that violate φ. (LTL → Büchi is a standard, if exponential, construction — ltl2ba, SPIN's -f, Spot's ltl2tgba.)
3. Build the product A_sys ⊗ A_¬φ. A run is accepted by the product iff it is a behaviour of the system and a violation of φ.
4. Check emptiness. φ holds for the system iff L(A_sys ⊗ A_¬φ) = ∅ — iff there is no behaviour that is both real and bad.

A Büchi automaton accepts an infinite run iff that run passes through an accepting state infinitely often. So the emptiness question becomes concrete and graph-theoretic:

Is there a reachable accepting cycle in the product automaton? An accepting state that lies on a cycle can be revisited infinitely often, yielding an accepting (= violating) infinite run.

LTL property:        []<>response          "always eventually response" (no starvation)
Negation ¬φ:         <>[]!response         "eventually, response is forever false"
Büchi A_¬φ:          a state that loops forever in !response, marked accepting
Violation found  ⇔   product has a reachable cycle through that accepting state

This is why explicit-state checkers are the natural home of liveness: temporal logic over infinite behaviours maps directly onto "find a reachable accepting cycle." Note the negation in step 2 — you build the automaton for the bad behaviours, so that finding a witness is finding a counterexample. A successful check is the failure to find any accepting cycle.

Key insight: Model checking LTL is automata intersection plus an emptiness test. φ holds iff System ∩ (behaviours violating φ) is empty. The counterexample, when it exists, is not a path to a bad state — it is an infinite run, represented finitely as a lasso.

Core Concept 3 — Nested DFS, Accepting Cycles, and the Lasso¶

How do you find a reachable accepting cycle without storing the whole product (which is |states_sys| × |states_¬φ|)? The classic answer is nested depth-first search (Courcoubetis–Vardi–Wolper–Yannakakis), and it is what runs inside SPIN.

The idea: an accepting cycle is a cycle that passes through some accepting state q. So (a) DFS the product to discover accepting states; (b) when the outer DFS finishes exploring an accepting state q (on its way back up), launch an inner DFS from q looking for a path back to q itself. If the inner search can reach a state on the outer DFS stack, you've closed a cycle through q — an accepting cycle.

NestedDFS(s0):
    outer_DFS(s0)
    report SAFE                        # no accepting cycle found anywhere

outer_DFS(s):
    mark s outer-visited
    for s' in succ(s):
        if s' not outer-visited: outer_DFS(s')
    if s is accepting:                 # post-order: subtree below s fully explored
        seed = s
        inner_DFS(s)                    # hunt for a cycle back to seed

inner_DFS(s):
    mark s inner-visited
    for s' in succ(s):
        if s' == seed or s' on outer-stack:
            report ACCEPTING CYCLE      # the lasso: outer-stack(→seed) + this-loop(→seed)
        else if s' not inner-visited:
            inner_DFS(s')

The counterexample it produces is a lasso:

        stem (finite)            loop (finite, repeated forever)
  s0 ──────────────────▶ q ◀───────────────────┐
                          │                      │
                          └──────────────────────┘
                          accepting state, revisited infinitely

  Infinite violating run = stem · loopᵂ   =  s0 … q (q+1 … q)^∞

The stem is the path from the initial state to the accepting state q (read off the outer DFS stack); the loop is the cycle from q back to q (read off the inner DFS). Together (stem, loop) finitely denote the infinite behaviour stem·loopᵂ. That is your liveness counterexample, and reading it is reading "here is how the system gets into a state from which it spins forever without making progress."

Two properties make nested DFS practical and beautiful:

• It's linear in the size of the product — O(|states| + |transitions|) — with only two extra bits per state (outer-visited, inner-visited).
• It's on-the-fly. You generate product states lazily during the DFS. The moment the inner search closes a cycle, you stop and emit the lasso — you never have to construct, let alone store, the full product. For a property that fails, you often touch a tiny fraction of the state space.

Key insight: The lasso (stem, loop) is the finite footprint of an infinite counterexample. Nested DFS finds one in linear time with two bits per state, on the fly — which is precisely why explicit-state checking of liveness is feasible at all despite the behaviours being infinite.

Core Concept 4 — State Hashing and Bitstate Supertrace¶

Even with linear-time search, Visited is the wall. SPIN's answer, bitstate hashing (Holzmann's supertrace), is one of the most pragmatic ideas in verification — and the trade-off it makes is the senior lesson.

Standard explicit-state stores each state (often compressed) in a hash table, comparing on collision so the result is exact. Bitstate hashing throws the states away. It allocates a giant bit array and, for each state, sets the bit(s) at one or more hash positions. "Have I seen this state?" becomes "are those bits already set?"

Exact hashing:     store full state, resolve collisions → SOUND (no missed states)
Bitstate (SUPERTRACE):
    bit[h1(state)] = 1; bit[h2(state)] = 1     # two hash functions (Bloom-filter style)
    "seen?"  ⇔  bit[h1]==1 AND bit[h2]==1

The catch is a hash collision: two distinct states map to the same set bits. The checker then believes it has already explored the second state and prunes it — skipping a whole subtree. If a bug lived in that subtree, the checker reports SAFE while a real counterexample exists. Bitstate hashing is therefore unsound: it can miss states, hence miss bugs.

What you get in return is staggering memory efficiency — a few bits per state instead of dozens of bytes, letting you cover state spaces orders of magnitude larger than fit in RAM exactly. And critically, the unsoundness is one-directional and quantifiable:

• A reported counterexample is always real (you only prune on a believed-seen state; emitting a bug requires actually reaching a bad state). No false alarms.
• A reported "no bug" is a probabilistic claim, and SPIN reports an estimated hash-factor / coverage (loosely, the fraction of the state space the bit array could distinguish). High coverage (the bit array large relative to the reachable states, double hashing) means a missed-state probability near zero; a low hash-factor means "you got a partial sweep, trust it accordingly."

Key insight: Bitstate/supertrace trades soundness for reach. It will never cry wolf, but its silence is only as trustworthy as the reported coverage. The senior move is to run exact when the state space fits, fall back to bitstate when it doesn't, and read the coverage number before believing a clean run — never report "verified" off a 12% hash-factor sweep.

This is the explicit-state world's escape valve. The symbolic world attacks the same memory wall from a completely different direction — not by approximating the set, but by representing it cleverly.

Core Concept 5 — Symbolic Model Checking with BDDs¶

The breakthrough that took model checking from 10⁵ to 10²⁰ states (McMillan, late 1980s) abandons enumeration entirely. Instead of storing individual states, symbolic model checking represents and manipulates sets of states as Boolean functions.

Encode each state as a bit-vector over Boolean variables x = (x₁…xₙ). A set of states is then a Boolean function — its characteristic function — that returns 1 exactly for the bit-vectors in the set. The transition relation is likewise a Boolean function T(x, x') over current-state vars x and next-state vars x', true iff there's a transition from x to x'. Now set operations become Boolean operations: union is ∨, intersection is ∧, complement is ¬.

The data structure that makes this fly is the (Reduced, Ordered) Binary Decision Diagram — a canonical DAG form of a Boolean function. ROBDDs are canonical (one BDD per function under a fixed variable order, so equality and "is this set empty/fixed?" are O(1) pointer checks) and frequently exponentially compact — a set of 10²⁰ states can be a BDD of a few thousand nodes when the set has structure.

The engine is image computation. The set of states reachable in one step from a set S:

Image(S)(x') = ∃x. ( S(x) ∧ T(x, x') )           # forward: successors of S
PreImage(S)(x) = ∃x'. ( S(x') ∧ T(x, x') )        # backward: predecessors of S

— all as BDD operations (conjunction, then existential quantification = "quantify out" the x variables). Reachability is then a fixpoint: keep adding the image until nothing new appears.

Reachable = Init
repeat:
    Next = Reachable ∨ Image(Reachable)
    if Next == Reachable: break        # FIXPOINT — O(1) BDD equality check
    Reachable = Next
# safety holds iff (Reachable ∧ Bad) == FALSE (the empty BDD)

The same fixpoint machinery checks CTL directly, with each operator as a least (μ) or greatest (ν) fixpoint of pre-image:

• EF p ("exists a path to p") = least fixpoint of p ∨ PreImage(·) — backward reachability from p.
• EG p ("exists a path where p holds forever") = greatest fixpoint of p ∧ PreImage(·) — repeatedly shrink to states that can stay in p.
• E[p U q] = least fixpoint of q ∨ (p ∧ PreImage(·)).

The make-or-break variable is BDD variable ordering. The same Boolean function can be a linear-size BDD under one ordering and an exponential blowup under another (the textbook example: an n-bit comparator is linear when corresponding bits are interleaved, exponential when all of one operand precedes the other). Symbolic checkers spend real effort on ordering heuristics and dynamic reordering (sifting) — and a symbolic check that explodes in memory has very often simply hit a bad order.

Key insight: Symbolic MC swaps "store the states" for "store a Boolean function over the states," and a BDD is the canonical, often-tiny encoding. The fixpoint engine is image/pre-image computation; the Achilles heel is variable ordering. This is why symbolic checking dominates control-heavy, data-light problems (hardware) and struggles when wide datapaths defeat the BDD.

BDDs hit their own wall on large datapaths and rich data types. The third family side-steps both enumeration and BDDs by handing the whole problem to a SAT solver.

Core Concept 6 — Bounded Model Checking with SAT/SMT¶

Bounded Model Checking (Biere, Cimatti, Clarke, Zhu, 1999) reframes the entire question as propositional satisfiability — and rides the spectacular progress of SAT/SMT solvers. The idea is almost shockingly direct: unroll the transition relation k steps and ask a solver whether a counterexample of length ≤ k exists.

Introduce a fresh copy of the state variables for each time step, s₀, s₁, …, s_k, and build one big formula:

BMC(k)  =   I(s₀)                              ∧   the run starts in an initial state
            ⋀_{i=0}^{k-1} T(s_i, s_{i+1})      ∧   each step is a legal transition
            ( ⋁_{i=0}^{k} ¬P(s_i) )            ←   the property is violated at SOME step ≤ k

Hand that to a SAT (or SMT) solver:

• SAT ⇒ the satisfying assignment is the counterexample — concrete values for s₀ … s_j showing exactly how the system reaches a bad state in j ≤ k steps. The solver hands you the trace.
• UNSAT ⇒ there is no counterexample of length ≤ k. (Crucially, not "the property holds" — only "no bug this short.")

For liveness, the property formula is replaced by a constraint asserting a loop within the k steps (⋁_l (s_k = s_l)) so the bounded unrolling can represent the lasso of an infinite violating run.

Why this was a revolution: it inherits all the engineering muscle of modern CDCL SAT solvers (and, via SMT, theories of bit-vectors, arrays, and arithmetic — so you can reason about machine integers, memory, and pointers natively, not bit-blasted by hand). It needs no BDDs and no good variable ordering. And it is the best bug-finder in the field: counterexamples tend to be shallow, so small k finds real bugs fast, and the solver's conflict-driven learning prunes the search far more aggressively than enumeration ever could.

A real CBMC-style invocation and the shape of what comes back:

// check: this never dereferences null and the assertion holds, for any input ≤ bound
void process(int *buf, unsigned n) {
    unsigned i = 0;
    while (i <= n) {            // off-by-one: writes buf[n] when array has n elements
        buf[i] = 0;
        i++;
    }
    __CPROVER_assert(i == n, "loop wrote exactly n elements");
}

$ cbmc bug.c --unwind 6 --bounds-check --pointer-check
** Results:
[process.array_bounds.1] line 4 buffer overflow on buf[i]: FAILURE
Counterexample:
  n = 3          (input chosen by the solver)
  i = 0 → 1 → 2 → 3 → 4        ← i reaches 4, buf[3] out of bounds for a 3-element array
  buf[3] = 0     ← the violating write
VERIFICATION FAILED

The solver chose n = 3 and walked the loop to expose the i <= n off-by-one. No state enumeration, no BDD — a single satisfiability query whose model is the bug.

Key insight: BMC turns "is there a bug?" into "is this formula satisfiable?" and the satisfying assignment is the counterexample. It is unbeatable at finding shallow bugs and, by itself, proves nothing — UNSAT at depth k means only "no bug ≤ k." Making BMC into a proof requires bounding k from above, which is the next concept.

Core Concept 7 — From Bounded to Complete: k-Induction and IC3/PDR¶

BMC at depth k finds bugs up to length k. To turn "no bug ≤ k" into "no bug, ever," you need to either bound k or replace unrolling with an inductive argument.

Completeness threshold / recurrence diameter. If there exists a k such that every reachable state is reachable within k steps — the completeness threshold, related to the recurrence diameter (the longest loop-free path in the state graph) — then BMC at that k is a complete proof: UNSAT there means UNSAT forever, because a longer counterexample would imply a shorter loop-free one already checked. The trouble: this k can be astronomically large and is itself hard to compute, so plain "BMC to the diameter" is rarely the practical route to a proof.

k-induction. A far more usable bridge. Ordinary 1-induction proves an invariant P with two SAT queries: base case I(s₀) ⇒ P(s₀) and inductive step P(s) ∧ T(s, s') ⇒ P(s'). The step often fails because P isn't inductive on its own — there's an unreachable "bad" state that satisfies P but steps to ¬P. k-induction strengthens the hypothesis over k consecutive steps:

Base:   no violation in the first k steps          (this is exactly BMC(k))
Step:   if P holds along ANY k consecutive states  s_i … s_{i+k-1}
        (and, in the simple-path variant, those states are pairwise distinct)
        then P holds at  s_{i+k}

The longer window lets you rule out the spurious predecessors that broke 1-induction, and the simple-path restriction makes it converge. k-induction is what tools like the SMT-based engines in CBMC (--k-induction) and many hardware checkers use to prove (not just bug-hunt) with a SAT/SMT backend.

IC3 / PDR (Property-Directed Reachability) — Bradley's IC3, the modern crown jewel of SAT-based unbounded model checking. It proves safety without any unrolling at all. Instead it incrementally builds a sequence of frames F₀, F₁, F₂, …, where each F_i is an over-approximation of the states reachable in ≤ i steps, refining them with the SAT solver:

IC3/PDR (sketch):
  F0 = Init
  loop:
    if a state in F_k can reach ¬P in one step (a CTI — counterexample-to-induction):
        try to PROVE that CTI unreachable by inductive generalization;
        push a learned clause (a generalized blocking lemma) BACK into earlier frames
        — or, if it can't be blocked, trace it to Init → REAL COUNTEREXAMPLE
    else add a new frame F_{k+1}
    if two adjacent frames become equal (F_i == F_{i+1}):   FIXPOINT → P PROVED

Two ideas make IC3 dominant. Incremental inductive generalization: when it learns a state is bad, it computes a small clause that excludes that state and many similar unreachable states, and proves that clause is inductive relative to the current frames — so each lemma does a lot of work. No unrolling: memory stays roughly constant in the bound, sidestepping BMC's blow-up at large k. IC3/PDR is the default engine in modern hardware model checkers and the backbone of competition-winning software verifiers.

Key insight: BMC alone is a bug-finder; k-induction and IC3/PDR are what make SAT-based checking a proof technique. IC3's trick — incrementally learning generalized inductive lemmas with no unrolling — is why it scales where BMC's growing formulas and BDDs' growing diagrams both stall.

Core Concept 8 — Predicate Abstraction and CEGAR¶

Real programs have unbounded data — 64-bit integers, heaps, recursion — so their concrete state space is infinite and direct enumeration is hopeless. Abstraction maps that infinite space to a small finite one; CEGAR automates choosing the right abstraction. Together they are the engine of modern software model checking (SLAM, BLAST, CPAchecker).

Predicate abstraction replaces a concrete state by the truth values of a finite set of predicates over program variables — e.g. { x > 0, lock == held, i < n }. A concrete state with x = 7, i = 2, n = 5 abstracts to the bit-vector (x>0)=T, (i<n)=T. The abstract model is finite (2^(#predicates) abstract states) and over-approximates the program: every concrete behaviour maps to an abstract one, so if the abstract model is safe, the program is safe. The danger is the reverse: the abstract model may have extra behaviours that no concrete run realizes — spurious counterexamples.

CEGAR — Counterexample-Guided Abstraction Refinement (Clarke, Grumberg, Jha, Lu, Veith) — closes the loop:

                ┌─────────────────────────────────────────────────────┐
                ▼                                                       │
   ┌────────────────────┐   safe    ┌──────────────────────────┐       │
   │ ABSTRACT the program│─────────▶│  PROGRAM IS SAFE (proof)  │       │
   │ over current preds  │          └──────────────────────────┘       │
   └─────────┬──────────┘                                              │
             │ abstract counterexample (CE)                             │
             ▼                                                          │
   ┌────────────────────┐  CE is REAL  ┌─────────────────────────┐     │
   │ CHECK if CE is      │─────────────▶│ REAL BUG (concrete trace)│     │
   │ feasible concretely │              └─────────────────────────┘     │
   └─────────┬──────────┘                                              │
             │ CE is SPURIOUS (infeasible on concrete program)          │
             ▼                                                          │
   ┌────────────────────────────────────────────────┐                  │
   │ REFINE: derive NEW predicates that rule the      │                  │
   │ spurious CE out  (often via CRAIG INTERPOLATION   │──────────────────┘
   │ of the infeasible path formula)                  │
   └────────────────────────────────────────────────┘

The refinement step is the clever part. When a path is spurious, its path formula (the conjunction of the statements' SMT encodings along the trace) is unsatisfiable — the concrete program can't actually follow it. A Craig interpolant of that unsatisfiable formula yields exactly the new predicate(s) needed to exclude the path in the next abstraction, without over-fitting. So CEGAR learns the predicates it needs, automatically, from the bugs it disproves — starting from no predicates and adding only what's necessary. This is why a tool like CPAchecker or SLAM can verify a device driver's locking discipline without a human ever writing down the abstraction.

Key insight: CEGAR is "abstract coarsely, check, and let the spurious counterexamples teach you what to refine." Predicate abstraction makes infinite programs finite; interpolation makes refinement automatic and targeted. The loop terminates with a proof, a real bug, or — since the underlying problem is undecidable — possibly not at all.

Core Concept 9 — Fighting the Explosion: POR, Symmetry, Compositional¶

State explosion is the enemy, and beyond hashing/symbolic/SAT there are three reductions every senior should recognise because they attack structural redundancy in the model.

Partial-Order Reduction (POR). In concurrent systems, most of the explosion is from interleaving independent actions. If thread A does x++ and thread B does y++ on disjoint variables, the orders A-then-B and B-then-A reach the same state and are equivalent for any property that doesn't observe the intermediate. POR explores only one representative interleaving per Mazurkiewicz-equivalence class, using ample sets (or persistent/stubborn sets) — at each state, a provably sufficient subset of enabled transitions to explore. It is the single most important reduction for concurrency and is built into SPIN by default; for asynchronous models it routinely turns an intractable check into a feasible one (often exponential savings).

Symmetry reduction. If a system has N interchangeable components — N identical clients, a ring of identical nodes — many states are identical up to permutation of component identities. Symmetry reduction quotients the state space by the symmetry group, exploring one canonical representative per orbit. For a protocol with N symmetric processes this can cut the space by up to N!.

Compositional / assume-guarantee reasoning. Rather than model-check the whole system M₁ ∥ M₂ (whose state space is the product of the parts), verify each component under an assumption about its environment, then discharge the assumptions:

   M₁  under assumption A   ⊨ φ        (M₁ satisfies φ if its environment behaves like A)
   M₂                       ⊨ A        (M₂ actually guarantees A)
   ───────────────────────────────
   M₁ ∥ M₂                  ⊨ φ        (so the composition satisfies φ)

This decomposes a product-sized problem into component-sized ones — the only structural hope for genuinely large systems, though finding the right assumption A is the hard, often-manual part (with active research on learning assumptions automatically).

Key insight: Hashing/symbolic/SAT shrink the representation of the state space; POR, symmetry, and compositional reasoning shrink the space itself by exploiting independence, interchangeability, and modularity. They compose with the engines — POR on top of explicit-state, symmetry on top of symbolic — and a real verification effort stacks several.

Core Concept 10 — Software Model Checking in Practice¶

Applying all of the above to actual code (not a hand-built model) splits into recognisable approaches, each with a representative tool and a characteristic challenge.

BMC of C — CBMC. The dominant approach for C/C++. It unwinds loops a fixed number of times, converts the program (with bounded loops) into an SMT formula over bit-vectors and arrays — machine integers with real overflow, memory as an array — and adds automatic checks (array bounds, null deref, overflow, user asserts). The signature artifact is the unwinding assertion: CBMC inserts an assertion that the loop bound was sufficient, so if a loop could run longer than --unwind k, it tells you rather than silently missing deeper bugs. Bug-finding is excellent; full proof requires loops to be genuinely bounded or paired with k-induction.

Bytecode execution — Java Pathfinder (JPF). A different design: JPF is a custom JVM that actually executes Java bytecode and backtracks the entire VM state at every nondeterministic choice (thread schedule, Verify.getInt() input). It explores all schedules and inputs by checkpoint/restore of the heap and stack. Great for finding concurrency bugs and NullPointerExceptions in real Java; the challenge is the cost of storing/restoring full VM states and the explosion of schedules.

Stateless model checking — CHESS, rr-style. For concurrency specifically, stateless checkers (Microsoft's CHESS, dynamic POR tools) abandon the visited set entirely. They re-execute the program under systematically different thread schedules, using a scheduler that controls every interleaving and dynamic POR to skip equivalent ones. No state hashing → no memory wall, at the cost of redoing work; this is the model behind deterministic-replay concurrency testing and is how many real-world races (TOCTOU, missing-lock, atomicity violations) get caught.

The deep, shared difficulty in all software model checking is unbounded data: the heap, pointers, and dynamic allocation. Aliasing (do p and q point to the same object?) makes the transition relation depend on facts that are themselves expensive to compute; an unbounded heap is an infinite state component. Tools cope with shape analysis, bounded heaps, separation logic, or SMT array theory — but "model checking with a rich heap" remains where these tools are weakest, and is exactly where abstraction (Concept 8) earns its keep.

Key insight: Software model checking is not one technique but a family: unroll-and-SMT (CBMC) for C, execute-and-backtrack (JPF) for bytecode, re-execute-under-controlled-schedules (CHESS) for concurrency. They share one nemesis — unbounded heap/pointers/data — which is why every practical software checker leans on bounding or abstraction.

Core Concept 11 — Liveness and Fairness in the Automata Framework¶

A subtlety that bites every senior who checks liveness on a concurrent model: most liveness properties are false without fairness, and the fix lives cleanly inside the automata framework.

Consider "every request eventually gets served." On a model with two processes, there's always a degenerate infinite run where the scheduler only ever runs process A and never schedules process B — so B's request starves, the property "fails," and the lasso you get back is a useless artifact of an unrealistic scheduler. The behaviour is real in the raw transition system but not in any fair execution.

Fairness constraints rule out these pathological runs:

• Weak fairness (justice): if a transition is continuously enabled from some point on, it must eventually be taken. (A process that is permanently ready to run won't be ignored forever.)
• Strong fairness (compassion): if a transition is enabled infinitely often, it must be taken infinitely often. (A process that keeps becoming ready, even intermittently, gets its turn.)

In the automata-theoretic setting these are not special cases — they're just more accepting conditions. The emptiness check becomes "is there a reachable cycle that is accepting and satisfies the fairness constraints?" — i.e. a cycle that, for each fairness requirement, contains the required transition. (Generalized Büchi automata with multiple accepting sets capture exactly this; SPIN exposes it via -f weak fairness, TLA+ via WF_vars/SF_vars conjoined into the spec.) The lasso must now thread through all the fairness sets to count as a genuine counterexample.

Key insight: Liveness without fairness almost always "fails" via a scheduler that starves someone — a counterexample that tells you nothing. Fairness is part of the specification, encoded as extra accepting conditions on the cycle. If your liveness check produces an obviously-unrealistic lasso, the first question is "did I forget to assert fairness?"

Real-World Examples¶

Amazon Web Services — TLA+/TLC (explicit-state). Engineers specified core protocols of DynamoDB, S3, and EBS in TLA+ and ran the TLC explicit-state checker over the reachable state space. TLC found subtle bugs — including a 35-step sequence of events that broke a replication invariant — that no test or review had caught, because the bug only manifested on one precise interleaving deep in the state space. The lesson AWS reports is exactly the one this page teaches: exhaustive exploration of a model finds design-level concurrency bugs that sampling (testing) structurally cannot. (Topic 03 goes deep on TLA+ itself.)

SPIN — explicit-state + nested DFS + bitstate. SPIN has verified communication and concurrency protocols across telecoms, spacecraft (NASA's flight-software verification), and OS kernels. It is the canonical home of nested-DFS liveness checking and of bitstate supertrace: when a protocol's exact state space won't fit, engineers fall back to supertrace and report the coverage — accepting a probabilistic clean run in exchange for sweeping a space that exact storage couldn't touch.

Hardware — symbolic (BDD) and IC3/PDR. Equivalence checking and property checking of CPU and ASIC designs is overwhelmingly control-heavy and data-light, which is the home turf of symbolic model checking. The SMV lineage (BDD-based) and modern IC3/PDR engines are standard in EDA flows; finding a corner-case pipeline-hazard bug pre-silicon is worth orders of magnitude more than finding it after tape-out.

Linux device drivers — CEGAR (CBMC/CPAchecker, SLAM heritage). Microsoft's SDV (Static Driver Verifier), built on SLAM, used predicate abstraction + CEGAR to verify that Windows drivers obey kernel API usage rules (acquire/release locking disciplines, IRQL constraints). It runs push-button on driver source, learning the predicates it needs from spurious counterexamples — the canonical industrial success of software model checking on real, heap-touching C.

Mental Models¶

• A safety checker is search with a visited set; a liveness checker is "find a reachable accepting cycle." Safety = "is a bad state reachable" (BFS/DFS + Visited). Liveness = "is there an infinite bad behaviour" = a lasso through an accepting state (nested DFS over the product). Whenever you read a liveness counterexample, you're reading a (stem, loop).

• Model checking LTL is intersection + emptiness. Build the automaton for the negation (the bad behaviours), intersect with the system, and ask "is it empty?" A passing check is the absence of any accepting run. The negation is why finding a witness is finding a bug.

• Three engines, three representations of the state space. Explicit-state enumerates it (and hashes/approximates to fit). Symbolic encodes it as a Boolean function (BDD) and iterates a fixpoint. SAT/BMC unrolls it into a satisfiability query. Match the engine to the problem: concurrency/liveness → explicit; control-heavy hardware → symbolic; deep shallow-bug-hunting on real code → SAT/BMC.

• BMC finds bugs; induction and IC3 prove their absence. UNSAT at depth k means only "no bug ≤ k." k-induction and IC3/PDR are the bridge from bounded bug-finding to an unbounded proof — IC3 by learning inductive lemmas with no unrolling at all.

• CEGAR is a learning loop. Abstract coarsely → check → if the counterexample is spurious, let it teach you the predicate that excludes it (interpolation) → repeat. The abstraction is discovered, not designed.

• You are verifying a model, not the system. Every result is "true of the abstraction I wrote." The algorithm is sound for the model; whether the model faithfully captures the system is a human responsibility no checker discharges.

Common Mistakes¶

1. Trusting a bitstate "no bug" without reading the coverage. Supertrace is unsound — collisions prune real states. A counterexample is always real; a clean run is only as trustworthy as the reported hash-factor/coverage. Run exact when it fits; never report "verified" off a low-coverage bitstate sweep.

2. Treating BMC UNSAT at depth k as a proof. It means "no counterexample of length ≤ k," nothing more. Without a completeness threshold, k-induction, or IC3, BMC proves absence of shallow bugs, not correctness. Conflating the two is the most common over-claim in SAT-based MC.

3. Checking liveness without fairness. Almost any liveness property "fails" via a scheduler that starves a process forever. The resulting lasso is an artifact, not a bug. Fairness (weak/strong, WF_/SF_, SPIN -f) is part of the specification — encode it before believing a liveness counterexample.

4. Verifying the wrong model (the abstraction gap). A model checker proves properties of the model you wrote. A model that quietly omits the failure mode, or mis-encodes the transition relation, yields a green check and false confidence. "I proved it correct" is only as strong as "I modelled the right thing."

5. Not checking that the property can actually fail (vacuity). If your invariant is trivially true — the antecedent is never satisfied, or the property is vacuously satisfied because some state is unreachable — the checker passes for the wrong reason. Always sanity-check: introduce a deliberate bug and confirm the checker catches it, and confirm the model is non-trivially satisfiable (reachable states exist; properties can be violated).

6. Expecting an infinite-state program to be decided. General software verification is undecidable; an unbounded heap or unbounded integers means no algorithm terminates on all inputs. That is why you bound (BMC, loop unwinding) or abstract (CEGAR) — not a tooling deficiency to engineer around.

7. Blaming the tool when a BDD or BMC explodes. A symbolic check that exhausts memory has very often hit a bad variable ordering; a BMC that stalls is fighting a deep counterexample or a wide datapath. The fix is frequently a different encoding/ordering/engine, not more RAM.

8. Ignoring counterexample length. A 600-step trace is undebuggable. Prefer BFS/shortest-counterexample modes; a minimal counterexample is the difference between "fixed in an hour" and "stared at it for a day."

Test Yourself¶

1. Explain why safety can be checked by reachability + a visited set, but liveness cannot. What is a liveness counterexample, structurally?
2. Walk through the automata-theoretic pipeline for checking an LTL property φ. Why do you negate φ and build an automaton for ¬φ? What does a passing check correspond to?
3. Nested DFS finds an accepting cycle. What are the roles of the outer and inner searches, and how does the algorithm read off the lasso's stem and loop?
4. Bitstate/supertrace hashing is unsound in one direction. Which direction, why, and what number must you read before trusting a clean run?
5. Write the BMC formula (schematically) for "no bad state within k steps." Given UNSAT at k = 20, exactly what have you proved — and what have you not?
6. 1-induction's step case fails on a perfectly safe property. Give a concrete reason why, and explain how k-induction (or IC3/PDR) fixes it.
7. In CEGAR, what makes a counterexample spurious, and how does interpolation turn a spurious counterexample into the refinement you need?
8. Your liveness check returns a lasso in which one process is simply never scheduled. What did you forget, and how do you encode the fix in the automata framework?

THE THREE ENGINES
  EXPLICIT-STATE   enumerate states into Visited (hash set); best for concurrency/liveness
                   SPIN, TLC.  Memory = |Visited|.
  SYMBOLIC (BDD)   represent SETS of states as Boolean functions; fixpoint over image/preimage
                   SMV lineage.  Best control-heavy/data-light (hardware).  Killer: var ordering.
  SAT/SMT (BMC)    unroll k steps → one satisfiability query; model = counterexample
                   CBMC, IC3/PDR.  Best shallow-bug-hunting on real code.

SAFETY vs LIVENESS
  safety   = "bad STATE reachable?"      → BFS/DFS + visited set (BFS = shortest CE)
  liveness = "bad BEHAVIOUR exists?"     → reachable ACCEPTING CYCLE = LASSO (stem + loop)

AUTOMATA-THEORETIC LTL
  ¬φ → Büchi A_¬φ  ;  product A_sys ⊗ A_¬φ  ;  φ holds ⇔ product language EMPTY
  emptiness = NESTED DFS (outer finds accepting states; inner finds cycle back) — O(n), on-the-fly

BITSTATE / SUPERTRACE (SPIN)
  store bits not states (Bloom-style)  → huge reach, UNSOUND (collisions miss states)
  counterexample always REAL ; "no bug" only as good as reported COVERAGE / hash-factor

BMC  =  I(s0) ∧ ⋀ T(s_i,s_{i+1}) ∧ ⋁ ¬P(s_i)        SAT ⇒ CE ; UNSAT ⇒ no bug ≤ k (NOT a proof)
  → proof via: completeness threshold (recurrence diameter) | k-INDUCTION | IC3/PDR (no unrolling)

CEGAR LOOP   abstract → check →  spurious? refine (interpolation) ↺  | real? BUG | safe? PROOF
  predicate abstraction = state ↦ truth of predicates {x>0, lock==held, …}

REDUCTIONS (shrink the space itself)
  partial-order (ample sets)   one interleaving per equivalence class   (SPIN default)
  symmetry                     one representative per orbit (÷ up to N!)
  assume-guarantee             M1 under A ⊨ φ ;  M2 ⊨ A  ⇒  M1∥M2 ⊨ φ

SOFTWARE MC
  CBMC  unwind loops + unwinding assertion + SMT(bit-vectors,arrays)   — C, bug-finding++
  JPF   custom JVM, executes bytecode, backtracks VM state             — Java schedules/inputs
  CHESS stateless: re-execute under controlled schedules + dynamic POR — concurrency races

ALWAYS CHECK
  - model faithfully captures the system (abstraction gap)
  - property CAN fail (vacuity): plant a bug, confirm it's caught
  - liveness has FAIRNESS (else scheduler-starvation false counterexamples)