# CBMC: The C Bounded Model Checker

arXiv: https://arxiv.org/abs/2302.02384 · HTML: https://mlsanity.com/paper/2302.02384/

## Key facts

- Cited by 12 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 5 Feb 2023.

## Built on by (most cited first, 12 of 12)

- [Neural Network Verification is a Programming Language Challenge](https://mlsanity.com/paper/2501.05867/) (2025)
- [A Contemporary Survey of Large Language Model Assisted Program Analysis](https://mlsanity.com/paper/2502.18474/) (2025)
- [Towards Reliable Code-as-Policies: A Neuro-Symbolic Framework for Embodied Task Planning](https://mlsanity.com/paper/2510.21302/) (2025)
- [Enhancing Automated Loop Invariant Generation for Complex Programs with Large Language Models](https://mlsanity.com/paper/2412.10483/) (2024)
- [NeuroCodeBench: a plain C neural network benchmark for software verification](https://mlsanity.com/paper/2309.03617/) (2023)
- [Quality Evaluation of COBOL to Java Code Transformation](https://mlsanity.com/paper/2507.23356/) (2025)
- [Floating-Point Neural Network Verification at the Software Level](https://mlsanity.com/paper/2510.23389/) (2025)
- [MFH: A Multi-faceted Heuristic Algorithm Selection Approach for Software Verification](https://mlsanity.com/paper/2503.22228/) (2025)
- [Cycle-Consistent Neural Explanation of Formal Verification Certificates](https://mlsanity.com/paper/2606.24414/) (2026)
- [T-LLM Compiler: Trusted LLM-based Code Optimization and Verification Framework](https://mlsanity.com/paper/2608.14953/) (2026)
- [Schwarz: Solver-Aware Agentic Program Verification](https://mlsanity.com/paper/2608.30803/) (2026)
- [Fewer Assumptions by Design: A Reusable Skill for LLM-Assisted Verus Verification](https://mlsanity.com/paper/2609.34886/) (2026)

## Abstract (arXiv)

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.