Source-linked AI summary
CBMC: The C Bounded Model Checker
Daniel Kroening, Peter Schrammel, Michael Tautschnig
TL;DR
A Boolean verification verdict and brief failure summary may not provide enough information to debug a program. CBMC computes counterexamples and prints execution traces; in the absolute-value example, the trace identifies the input that triggers signed overflow.
Problem
A Boolean verdict and one-line failure summary are typically insufficient for a software engineer to debug the reported problem.
Source: §2 · p. 4Method
CBMC computes full counterexamples and prints execution traces, including input values that trigger failed assertions.
Source: §2 · pp. 4–5Results
In the absolute-value example, the trace identifies the maximum negative 32-bit two’s-complement input that triggers arithmetic overflow.
Source: §2 · p. 5Takeaways & Limitations
Counterexample traces provide execution and input details beyond the Boolean verdict, supporting debugging of reported failures.
Source: §2 · pp. 4–5Automatic loop-bound detection may fail for highly data-dependent iterations, and loops may be too large or unbounded, requiring a chosen maximum unwind count.
Source: §5.3 · p. 26
Abstract
from arXiv · showhide
The C Bounded Model Checker (CBMC) demonstrates the violation of assertions in C programs, or proves safety of the assertions under a given bound. CBMC implements a bit-precise translation of an input C program, annotated with assertions and with loops unrolled to a given depth, into a formula. If the formula is satisfiable, then an execution leading to a violated assertion exists. CBMC is one of the most successful software verification tools. Its main advantages are its precision, robustness and simplicity. CBMC is shipped as part of several Linux distributions. It has been used by thousands of software developers to verify real-world software, such as the Linux kernel, and powers commercial software analysis and test generation tools. Table 1 gives an overview of CBMC's features. CBMC is also a versatile tool that can be applied to solve many practical program analysis problems such as bug finding, property checking, test input generation, detection of security vulnerabilities, equivalence checking and program synthesis. This chapter will give an introduction into CBMC, including practical examples and pointers to further reading. Moreover, we give insights about the development of CBMC itself, showing how its performance evolved over the last decade.
1 Introduction
CBMC translates C programs with assertions into a bit-precise formula to find assertion violations or prove safety under a bound. The chapter introduces its practical uses and development, including performance evolution over the last decade.
1 Introduction
- CBMC bit-precisely translates an annotated C program, with loops unrolled to a given depth, into a formula whose satisfiability indicates an assertion-violating execution.It can also prove assertion safety under the given bound.Source: §1 · p. 1
- CBMC is used to verify real-world software, including the Linux kernel, and powers commercial software analysis and test-generation tools.The authors cite its precision, robustness, and simplicity as advantages.Source: §1 · p. 1
- Table 1 gives an overview of CBMC’s features.Source: §1 · p. 1, Table 1 · p. 2
- Applications include bug finding, property checking, test-input generation, security-vulnerability detection, equivalence checking, and program synthesis.Source: §1 · p. 1
- The chapter covers CBMC’s verification approach, tutorial examples, real-world applicability, architecture, and performance evolution over ten years.It also describes the CPROVER framework, implemented in C++ at about 250 KLOC and available under a BSD-style license.Source: §1 · pp. 1–2
2 Verification Approach
CBMC applies bounded model checking to C programs by encoding bounded executions and assertions as a formula. A satisfiable formula yields a counterexample, as the absolute-value example demonstrates with signed overflow.
2 Verification Approach
- CBMC represents a C program’s bounded execution steps through loop and recursive-call unrolling, with assertions serving as specifications.The C program supplies the transition relation and its entry point determines the initial state.Source: §2 · p. 2
- CBMC reduces bounded program-path questions to SAT or SMT constraints; with a SAT back end, a satisfying CNF model describes a path violating an assertion.For bounded model checking generally, completeness requires a finite number of steps to reach all states; soundness is achieved by incrementing the bound until a witness is found.Source: §2 · p. 2
- A successful verdict can be vacuous when no assertions generate verification conditions; enabling signed-overflow checks generates a condition and reveals the example’s failure.The example’s solver finds the formula satisfiable, and CBMC reports the violated overflow assertion.Source: §2 · pp. 3–4
- CBMC’s counterexample trace prints the execution steps leading to a failed assertion and the input value that triggers the overflow.The printed binary value identifies the maximum negative number representable in 32-bit two’s complement.Source: §2 · p. 5
- The absolute-value example exposes signed overflow on the minimum negative 32-bit input, which CBMC prints in its counterexample trace.The overflow occurs when the program evaluates -x.Source: §2 · p. 5
3 Using CBMC
This section shows how CBMC supports C program verification through assertions, generated properties, built-in modeling facilities, and constraints on program paths. Examples cover bounded-loop and safety checks, test-suite generation and coverage, and concurrency-error detection with pthread support.
3 Using CBMC
- CBMC checks programmer assertions or generated potential-bug assertions for memory, pointer, leak, arithmetic, floating-point, and shift properties; violations are reachability paths that can be inspected like debugger traces.Generated assertions come from conservative static analysis and require model checking to confirm whether they represent genuine bugs.Source: §3 · p. 6
3.1 Handling Loops
- For complete bounded verification, loops need finite runtime bounds and sufficient unwinding, which CBMC can check; limiting unwinding instead supports bug hunting without proving correctness.In the lock example, a bound of one finds no bug, but a bound of two finds an assertion violation; lower bounds can fail unwinding assertions when more iterations are possible.Source: §3.1 · pp. 7–8
3.2 Using Built-in Checks
- CBMC’s bounds and pointer checks detect the login example’s out-of-bounds write at index 16; its counterexample provides triggering inputs, while restricting input to 15 characters makes all properties pass.Static analysis generates properties that may be imprecise, and SAT solving determines whether they hold; failed checks can produce a trace ending at the faulty access.Source: §3.2 · pp. 10–11
3.3 Built-In Functions and Types
- __CPROVER_assert can attach descriptions to properties, while __CPROVER_assume constrains nondeterministic choices; assumptions affect only later properties and must be satisfiable to avoid vacuous verification.An assumption on an execution path that evaluates false aborts that path without failure.Source: §3.3 · p. 12
- Assumptions constrain only subsequent assertions, and nondeterministic choice cannot provide universal quantification: ensuring a[x]>=0 for some index does not ensure the same for y.The example’s assertion fails because x and y need not have the same value.Source: §3.3 · pp. 12–13
- CBMC provides arbitrary fixed-size bit-vector, IEEE-754 floating-point, and fixed-point types, with configurable floating-point rounding mode.The float type specifies total and mantissa sizes; the fixed-point type specifies total and fractional sizes.Source: §3.3 · p. 13
3.4 Built-In Library
- CBMC ships definitions for commonly used library functions, often over-approximating their standard-prescribed behavior, and supports pthread programs for model checking.The bank-account example can be checked by running cbmc account.c.Source: §3.4 · p. 14
- The account example exhibits a race condition: thread 1 withdraws 3000 and sets the balance to -1000, but thread 2 overwrites it using the initial balance, yielding 9000 rather than expected 6000.Source: §3.4 · p. 15
3.5 Test Inputs
- CBMC generates tests for coverage criteria such as MC/DC, branch, and condition coverage, and supports custom criteria through __CPROVER_cover(condition).The section describes MC/DC test generation for a PID controller program.Source: §3.5 · pp. 15, 18
- The generated pid.c test suite achieves close to 100% MC/DC coverage, though it does not cover main’s return statement.The test inputs required at each time step are listed for each test.Source: §3.5 · p. 17
4 Verifying Real-World Software
goto-cc makes verification of real-world software projects easier by collecting build outputs into models CBMC can analyze. Its hybrid binaries preserve ordinary compiler and linker workflows while carrying verification models.
4 Verifying Real-World Software
- goto-cc collects project models through existing build steps, addressing projects’ many source files, libraries, and configuration options.It preprocesses source, parses it into goto programs, and interprets relevant compiler command-line options.Source: §4 · p. 18
- Embedding intermediate representations in executable files lets normal renaming, archiving, and linking apply to both code and verification models.The resulting approach enables running CBMC on Linux distribution packages.Source: §4 · pp. 18–19
- goto-cc can link multiple model files into a model library, which an object file can then link against.Its linker mode can replace common system linkers on Linux, Mac, and Windows.Source: §4 · p. 19
5 Architecture
CBMC transforms bounded program executions into solver formulas to check assertions. Its architecture includes command-line configuration, language front ends, symbolic execution, and SAT or SMT back ends.
5 Architecture
- CBMC translates program paths into constraints; with the SAT back end, solutions to its CNF formula describe paths violating assertions.Figure 2 outlines the main steps in this process.Source: §5 · p. 19, Figure 2 · p. 19
5.1 Command-line Front End
- The command-line front end configures CBMC, including entry point, source paths, macros, type widths, endianness, platform, and loop-unwinding limits.If not overridden, the architecture configuration defaults to the platform on which CBMC was compiled.Source: §5.1 · p. 20
5.2 Language Front End
- Language front ends parse and type-check input, then translate it into GOTO programs with guarded control flow and instrumented property checks.CBMC also transforms returns and resolves function pointers through a lightweight static analysis.Source: §5.2 · pp. 21, 23
5.3 Symbolic Execution
- CBMC eagerly unwinds loops to fixed bounds, converts GOTO functions to SSA, and bit-precisely encodes the resulting guarded equations.Automatic bound detection can unwind some loops to completion, but may fail for highly data-dependent iteration counts; users can set a maximum with --unwind B.Source: §5.3 · pp. 24–26
5.4 SAT/SMT Back Ends
- The back end translates guarded equations into CNF for SAT solvers or another encoding for SMT solvers; satisfying assignments yield violating paths, while unsatisfiability rules out violations within the bounds.CBMC reconstructs a counterexample trace from the satisfying model and guarded statements.Source: §5.4 · p. 26
6 Performance History
Across 22 CBMC versions, SV-COMP scores improved substantially over more than nine years, through successive periods of improvement rather than a few dominant feature releases. Performance gains varied by benchmark category and reflected both incremental changes and targeted improvements.
6 Performance History
- The benchmark used 22 versions across nine SV-COMP categories under fixed resource limits, but its scores are not comparable to official SV-COMP results because rules and benchmark sets changed.The versions ranged from CBMC 4.0 (June 2011) to 5.20 (December 2020); the runs used limits of 15 GB and 900 seconds.Source: §6 · p. 27
- SV-COMP scores improved substantially across more than nine years, with major waves in 2014–2015 and 2017–2018.The earlier wave compared versions from 2011–2013 with those from 2014–2015; another improvement wave appeared from versions 5.7 to 5.9.Source: §6 · pp. 27–28
- CPU-time gains through CBMC 5.0 and from 5.7 to 5.9 coincided with major peak-memory reductions, while intervening versions included stagnation and regressions.The CPU-time quantile plot shows a regression in 5.4 and another in 5.8; later versions brought smaller speed improvements.Source: §6 · p. 28, Figure 4 · p. 28, Figure 5 · p. 28
- Expression simplification before SSA-to-SAT encoding contributed to improvements, and CBMC 5.9’s on-demand compiler-built-in definitions saved half a second on short-running benchmarks.The half-second speed-up is described as constant and visible on benchmarks with short runtimes.Source: §6 · p. 29
- Performance varied by category: ReachSafety-Loops changed little, while MemSafety-Heap became faster and produced fewer incorrect results.For MemSafety-Heap, incorrect results fell from a sixth in CBMC 4.6 to a single result since CBMC 5.9.Source: §6 · pp. 29–30, Figure 7 · p. 29, Figure 6 · p. 29
- Floating-point decision-procedure fixes and optimizations, plus CBMC 5.8’s fuller math.h library, helped later 5.x versions solve more ReachSafety-Floats benchmarks.The sustained period of floating-point fixes and optimizations was especially notable between CBMC 4.2 and 5.0.Source: §6 · p. 30
- CBMC’s long-term gains came from a steady stream of incremental enhancements and bug fixes, not a few massive feature-driven boosts.Recent improvements were attributed to symbolic-execution enhancements, including optimized constant propagation and points-to data structures and more precise propagation for structures and arrays.Source: §6 · p. 30
7 Future Directions
CBMC can verify and find bugs in large software projects, but applying it in that setting is difficult and often requires expert users and substantial manual work. Development therefore focuses on improving usability alongside performance.
7 Future Directions
- Applying CBMC to large software projects often requires expert users and substantial manual work to decompose applications and write realistic harnesses and stubs.The harnesses and stubs must model assumptions about the program’s execution environment.Source: §7 · pp. 30–31
- CBMC has been used to verify and find bugs in real, large-scale software projects.Source: §7 · p. 30
- Alongside continued performance improvements, improving usability for CBMC users is a main development focus.Source: §7 · p. 31