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.

翻译：C有界模型检测器（CBMC）可验证C程序中断言违反的情况，或在给定界限下证明断言的安全性。CBMC将输入C程序（包含带断言标注且循环展开至指定深度的代码）通过逐位精确的转换转化为公式。若该公式可满足，则存在一条导致断言违反的执行路径。CBMC是最成功的软件验证工具之一，其主要优势在于精确性、鲁棒性和简洁性。CBMC已作为多个Linux发行版的组成部分发布，被数千名软件开发者用于验证如Linux内核等真实世界软件，并驱动着商业软件分析与测试生成工具。表1概述了CBMC的功能特性。CBMC亦是可应用于解决多种实际程序分析问题的通用工具，涵盖缺陷发现、属性检查、测试输入生成、安全漏洞检测、等价性检查及程序合成。本章将介绍CBMC基础内容，包含实践案例及拓展阅读指引。此外，我们将深入解析CBMC自身的发展历程，展示其过去十年间性能演进的脉络。