cbmc-starter-kit

CBMC starter kit

This is a starter kit for writing CBMC proofs.

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, which means that the set of all possible inputs may have to be restricted to all inputs of some bounded size.

The starter kit overview gives a fairly complete example of how to use the starter kit to add CBMC verification to an existing software project.

The starter kit wiki is currently the primary user guide for the starter kit.

Installation

The starter kit is distributed as both a brew package and a pip package, and the release page gives installation instructions that we repeat here.

brew installation

On MacOS, we recommend using brew to install the starter kit with

brew tap aws/tap
brew install cbmc-starter-kit

and upgrade to the latest version with

brew upgrade cbmc-starter-kit

In these instructions, the first line taps an AWS repository that hosts the starter kit. The brew home page gives instructions for installing brew.

pip installation

On any operating system with python installed, use pip to install the starter kit with

python3 -m pip install cbmc-starter-kit

and upgrade to the latest version with

python3 -m pip install --upgrade cbmc-starter-kit

The python download page gives instructions for installing python.

Security

See CONTRIBUTING for more information.

License

This project is licensed under the Apache-2.0 License.