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.
2 maintainers
Metadata
2 maintainers
Release files for cbmc-starter-kit 2.10
For a detailed explanation of source distributions (sdists) and built distributions (wheels), please see the package formats documentation.
Source distribution (sdist)
| File | Size | Uploaded | |
|---|---|---|---|
| cbmc-starter-kit-2.10.tar.gz | 40.6 kB | Details |
Built distribution (wheel)
| File | Interpreter | ABI | Platform | Reset |
|---|---|---|---|---|
| cbmc_starter_kit-2.10-py3-none-any.whl | Python 3 | none | any | Details |
Total release size: 105.8 kB
Release files / cbmc-starter-kit-2.10.tar.gz
| Download URL | cbmc-starter-kit-2.10.tar.gz |
|---|---|
| Size | 40.6 kB |
| Tags | Source |
|
SHA-256 checksum How to use checksums |
65b36edd6a269d1fde34fc7643e69d52a462dd878a265d8aa43662c97f5299ee
|
|
BLAKE2b-256 checksum How to use checksums |
15e12b0714b33baa5dc2221cf428f58aaddef8e308dd9d41d74145a0d3f1d8e2
|
| Upload date | |
|
Uploaded using Trusted Publishing? What is trusted publishing? |
No |
| Uploaded via |
twine/4.0.2 CPython/3.8.10
|
Release files / cbmc_starter_kit-2.10-py3-none-any.whl
| Download URL | cbmc_starter_kit-2.10-py3-none-any.whl |
|---|---|
| Size | 65.3 kB |
| Tags | Python 3 |
|
SHA-256 checksum How to use checksums |
7f18a78ab3dab412bffc6d059ccda55a90c031b4a34f425f9fbc4f7584e4cc0d
|
|
BLAKE2b-256 checksum How to use checksums |
7ee552192467b4cfb9f0b5cfeb7e6f4fa0081564f93af2d66cf92e933c413203
|
| Upload date | |
|
Uploaded using Trusted Publishing? What is trusted publishing? |
No |
| Uploaded via |
twine/4.0.2 CPython/3.8.10
|
