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:

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:

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:

Last modified: 2023-09-22 12:00:47 -0700