Bounded Model Checking

Origin. Biere, Cimatti, Clarke, Zhu (1999). Unroll transition relation k times. SAT encoding of bounded reachability. No state explosion for bounded depth. Foundation for industrial verification.

Models. Check property up to bound k. Path of length k as propositional formula. SAT solver finds bugs. Incremental deepening. Complete for finite systems with known diameter.

Formalism.

Transition system: M = (S, I, T) where:

S: states (propositional variables)
I(s): initial states
T(s, s'): transition relation

BMC encoding: Unroll k steps: I(s₀) ∧ T(s₀, s₁) ∧ ... ∧ T(sₖ₋₁, sₖ)

Safety property: ¬(I(s₀) ∧ ⋀ᵢT(sᵢ, sᵢ₊₁) ∧ ⋁ᵢ¬P(sᵢ)) UNSAT iff no counterexample of length ≤k.

Liveness (bounded): Find lassos: path to loop. l ≤ k: loop-back position. Büchi acceptance in loop.

Incremental BMC: k = 0, 1, 2, ... Reuse learned clauses. Stop at diameter or resource limit.

Completeness: Diameter d: longest shortest path. If SAT for all k ≤ d: property holds. Recurrence diameter: harder to compute.

Interpolation for completeness: Craig interpolants from UNSAT proofs. Approximate reachability. McMillan's approach.

Symbols.

Symbol	Unicode	Name	Meaning
k	—	Bound	Unrolling depth
M	—	Model	The transition system (S, I, T)
S	—	State space	Encoded by propositional variables
I	—	Initial	Predicate holding of initial states
T	—	Transition	Step relation T(s, s′)
P	—	Property	Safety predicate on a state
sᵢ	—	Indexed state	Copy of the state variables at step i
⋀	U+22C0	N-ary logical and	Conjunction over the unrolled steps
⋁	U+22C1	N-ary logical or	Disjunction over the positions checked
∧	U+2227	Logical and	Binary conjunction in the encoding
¬	U+00AC	Not sign	Negation of the property or the whole encoding
≤	U+2264	Less-than or equal to	Counterexample length bound; loop-back position
l	—	Loop-back position	Where a lasso re-enters its cycle
d	—	Diameter	Longest shortest path between reachable states
SAT	—	Satisfiable	A model exists, hence a concrete counterexample trace
UNSAT	—	Unsatisfiable	No model, hence no counterexample of length ≤ k

Metatheory. Soundness is immediate and one-sided: a satisfying assignment to the unrolled formula is a concrete trace of the system, so every reported counterexample is real. What UNSAT at bound k establishes is only the absence of counterexamples of length at most k, and Biere, Cimatti, Clarke, and Zhu's 1999 contribution was the observation that this partial answer is worth having, because the encoding is linear in k and in the size of T while the underlying symbolic reachability problem for a system presented as a propositional transition relation is PSPACE-complete. The bounded question is instead a sequence of NP-complete SAT instances (Cook 1971, Levin 1973), and modern incremental solvers reuse learned clauses as k increases. Completeness is recovered by a completeness threshold: the diameter for safety, the larger recurrence diameter for lasso-shaped liveness counterexamples, analysed by Clarke, Kroening, Ouaknine, and Strichman (2004). McMillan (2003) gave the alternative — Craig interpolants extracted from the UNSAT proof yield an inductive invariant without computing any threshold.

Applies to. Hardware verification. Software BMC (CBMC). Security (fuzzing guidance). Bug finding. Test generation.

Limitations. The method is a refutation procedure: UNSAT at bound k proves nothing about the system, only about traces of length ≤ k, so a violation first reachable beyond any feasible bound is indistinguishable from correctness. Recovering a proof needs a completeness threshold, and the diameter is not easily obtainable — checking that a candidate d is the diameter is a quantified rather than an existential Boolean question — while the recurrence diameter that liveness requires can be exponentially larger. The encoding grows linearly in k but solving time does not, so the bound at which the search stops is set by the solver, not by the property. Infinite-state programs must be finitized before encoding — bounded integers, bounded heap, bounded loop unwinding — so what is decided concerns the finitization, and only an unwinding assertion reveals that the finitization was too small.