Skip to content

Software Quality

Bounded model checking

Bounded model checking (BMC) (Biere et al. 1999)1 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 (C, C++) and JBMC (Java) unwind the program and discharge assertions, array-bounds, and pointer-safety checks to a SAT or SMT solver.
  • Hardware / RTL. SymbiYosys drives Yosys-based bounded and k-induction property checking on Verilog and SystemVerilog; EBMC is a bounded model checker for the same. JasperGold (Cadence) is a commercial RTL property checker.

Relationship to neighbors

BMC and symbolic execution 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 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 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 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)2.
  • 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.

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

They share a name but check different things. Model checking 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 works on a spec or model and is exhaustive over it. Symbolic execution 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 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

References

  1. Biere, Armin, Alessandro Cimatti, Edmund Clarke, and Yunshan Zhu. 1999. "Symbolic Model Checking without BDDs." 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. ↩

  2. Cook, Byron, Kareem Khazem, Daniel Kroening, Serdar Tasiran, Michael Tautschnig, and Mark R. Tuttle. 2020. "Model Checking Boot Code from AWS Data Centers." Formal Methods in System Design 57 (1): 34–52. https://doi.org/10.1007/s10703-020-00344-2. ↩