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.
CBMC has been used on over a dozen industrial software verification projects as a routine part of software development and continuous integration. This experience has resulted in some "best practices" for how to build software for CBMC and how to run CBMC in development. The CBMC starter kit is an implementation of these best practices, and is intended to make it easy to deploy CBMC to a software project as part of software development and continuous integration.
This document is a guide to using CBMC and to deploying CBMC to an industrial software verification project.
For a quick start on writing proofs that includes simple exercises, read
- Read configure the repository to set up a software repository for CBMC proof
- Read configure the proof to add a new CBMC proof to an existing set of CBMC proofs
- Read run all proofs to run a set of existing CBMC proofs and examine the results.
For advice on planning and managing a CBMC proof project, read CBMC project management.
- CBMC starter kit reference manual and documentation
- CBMC viewer reference manual and documentation
- CBMC developer guide
- Litani reference manual
This training material is a work in progress. If you have suggestions, corrections, or questions, please contact us by submitting a GitHub issue. If you have some training of your own that you would like to contribute, please submit your contributions as a GitHub pull request.