# Bounded model checking

Bounded model checking (BMC) (Biere et al. 1999)[^biere1999] unrolls a program to a fixed depth *k*
and asks a SAT or SMT solver whether any execution within that bound violates an
assertion. Within the depth *k* a clean run is a proof that no assertion fails,
and beyond *k* it claims nothing, because loops and recursion are unwound only
*k* times.

## What it catches

- **Assertion violations.** Any reachable state within depth *k* that fails a
  written assertion or safety property.
- **Memory-safety bugs.** Buffer overflows, out-of-bounds array access, null and
  invalid pointer dereferences, arithmetic overflow.
- **RTL property violations.** Assertion and safety-property failures in a
  Verilog or SystemVerilog design, up to a bounded number of cycles.

What it does *not* catch is any bug that first appears deeper than the unwinding
bound.

## Tools

- **Software.** [CBMC](https://www.cprover.org/cbmc/) (C, C++) and [JBMC](https://www.cprover.org/jbmc/) (Java) unwind the
  program and discharge assertions, array-bounds, and pointer-safety checks to a
  SAT or SMT solver.
- **Hardware / RTL.** [SymbiYosys](https://github.com/YosysHQ/sby) drives Yosys-based bounded and
  k-induction property checking on Verilog and SystemVerilog; [EBMC](https://github.com/diffblue/hw-cbmc)
  is a bounded model checker for the same. JasperGold (Cadence) is a commercial
  RTL property checker.

## Relationship to neighbors

BMC and [symbolic execution](https://quality.stereobooster.com/symbolic-execution.md) both unroll code and call a
solver: BMC poses one query over the whole program unrolled to depth *k*,
while symbolic execution explores feasible paths one at a time. Spec-level
[model checking](https://quality.stereobooster.com/model-checking.md) proves a property of a *model* that must be
kept faithful to the code, while BMC proves a property of the *code* but only to
depth *k*. The same unrolling also underlies bounded
[equivalence checking](https://quality.stereobooster.com/equivalence-checking.md) of two implementations.

## When to use, when not

**Use:**

- C/C++/Java or RTL with written assertions, where memory safety or a safety
  property must hold and the interesting behavior fits within a reachable depth.
- When an exhaustive verdict on the *implementation* is wanted without writing
  and maintaining a separate abstract model.

**Don't:**

- When the suspected bug lies deeper than a feasible unwinding depth: BMC
  returns a clean verdict that says nothing about it.
- When the design is better abstracted than checked directly: a spec-level
  [model](https://quality.stereobooster.com/model-checking.md) reaches the distributed-protocol interleavings a
  bounded unrolling of the implementation cannot.

## Evidence

- **AWS boot code proved memory-safe.** CBMC proved the initial boot code
  running in Amazon Web Services data centers memory-safe, solving obstacles
  specific to boot code (memory-mapped device interfaces, byte-level memory
  access, linker-script memory layout) that standard static-analysis tools cannot
  easily handle without modification (Cook et al. 2020)[^cook2020].
- **Comparative effectiveness.** How much BMC finds depends on the unwinding
  depth a program admits, so its effectiveness is hard to separate from the
  program it was run on.

## Related

**Same name, different thing — Model checking vs bounded model checking**

They share a name but check different things. [Model
checking](https://quality.stereobooster.com/model-checking.md) explores an abstract *model* or spec
exhaustively against a temporal or safety property: the model is small enough to
explore in full, but a passing run says nothing about whether the implementation
matches it. Bounded model checking
checks the *implementation itself*, unrolled to a fixed depth *k*: there is no
model-fidelity gap, but the verdict holds only up to depth *k*. Model checking
trades implementation-fidelity for unbounded exploration of a model; bounded
model checking trades depth for checking the real code.

**Exploring the program's behavior space**

All explore many program behaviors; they differ in what they run and what they
guarantee. [Model checking](https://quality.stereobooster.com/model-checking.md) works on a spec or
model and is exhaustive over it. [Symbolic
execution](https://quality.stereobooster.com/symbolic-execution.md) runs the *actual code*, solving
path constraints to reach branches a fuzzer can't, with a bounded-exhaustive
verdict; bounded model checking runs
the actual code too, but poses a single SMT query over the whole program unrolled
to a fixed depth rather than exploring paths one at a time.
[Fuzzing](https://quality.stereobooster.com/fuzzing.md) runs the actual code too but samples inputs
empirically: cheaper per case, no exhaustiveness claim.

## Classification

- **Quality dimensions:** Functionality, Reliability.
- **Area:** Implementation-level verification of C/C++/Java code and of hardware RTL (Verilog/SystemVerilog): assertions, memory safety, and equivalence, up to a bounded execution depth.
- **Guarantee:** Exhaustive to the unwinding depth k — a proof of assertion-freedom within the bound, on the implementation itself.

## Referenced by

- [Dead-code detection](https://quality.stereobooster.com/dead-code-detection.md) · Methods
- [Model checking](https://quality.stereobooster.com/model-checking.md) · Methods
- [Symbolic execution](https://quality.stereobooster.com/symbolic-execution.md) · Methods
- [Verifying memory safety](https://quality.stereobooster.com/memory.md) · Methods
- [Verifying safety-critical systems](https://quality.stereobooster.com/safety.md) · Methods

## References

[^biere1999]: Biere, Armin, Alessandro Cimatti, Edmund Clarke, and Yunshan Zhu. 1999. "[Symbolic Model Checking without BDDs](https://www.cs.cmu.edu/~emc/15-820A/reading/biere99symbolic.pdf)." *Tools and Algorithms for the Construction and Analysis of Systems (TACAS 1999)*, Lecture notes in computer science, vol. 1579: 193–207. [https://doi.org/10.1007/3-540-49059-0\\\_14](https://doi.org/10.1007/3-540-49059-0\_14).
[^cook2020]: Cook, Byron, Kareem Khazem, Daniel Kroening, Serdar Tasiran, Michael Tautschnig, and Mark R. Tuttle. 2020. "[Model Checking Boot Code from AWS Data Centers](https://link.springer.com/content/pdf/10.1007/s10703-020-00344-2.pdf)." *Formal Methods in System Design* 57 (1): 34–52. <https://doi.org/10.1007/s10703-020-00344-2>.

## Acronyms

- BDD — behavior-driven development
- BMC — bounded model checking
- RTL — register-transfer level
- SAT — Boolean satisfiability
- SMT — satisfiability modulo theories