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
I	—	Initial	Initial states
T	—	Transition	Step relation
SAT	—	Satisfiable	Has model
UNSAT	—	Unsatisfiable	No model

Metatheory. Sound: counterexamples are real. Complete for bounded depth. SAT complexity. Incremental solving crucial. Parallel/distributed variants.

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

Limitations. Incomplete for unbounded. Large bounds expensive. Liveness harder. Diameter unknown. Memory for unrolling.