CBMC quick start

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.

Getting started

For a quick start on writing proofs that includes simple exercises, read

For a quick start on deploying CBMC to a software project, we recommend that you read our tutorial, but if you want to dive right in, you can install the tools and

For advice on planning and managing a CBMC proof project, read CBMC project management.

To learn more, see our list of CBMC resources and CBMC projects, and see

Helping others

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.