CBMC is a model checker for C. This means that CBMC will explore all possible paths through your code on all possible inputs, and will check that all assertions in your code are true. CBMC can also check for the possibility of memory safety errors (like buffer overflow) and for instances of undefined behavior (like signed integer overflow). CBMC is a bounded model checker, however, and using CBMC may require restricting inputs to inputs of some bounded size. The result is assurance that your code behaves as expected for all such inputs.

This page is the root of all documentation for CBMC:

The Installation Guide describes how to install CBMC
The User Guide describes what you need to know to use CBMC
The Reference Guide describes the CBMC tools
The Developer Guide describes what you need to know to contribute to CBMC

CBMC documentation has traditionally been generated from doxygen comments in the source code and a few additional markdown files. Over time, we will move this documentation into the guides listed above, but for now, this source code documentation is avilable here:

CProver documentation

CBMC documentation will never be done. If you learn something interesting or find a mistake, please consider contributing documentation with a pull request or describing the problem to us by filing an issue. Some advice on contributing documentation is available here:

Contributing documentation

Last modified: 2024-12-16 13:58:47 -0800