For a quick start with CBMC on simple problems, read
For a quick start with CBMC on large software projects, read
Two third-party tools simplify using CBMC:
- CBMC Viewer scans the output of CBMC and produces a browsable summary of its findings.
- CBMC Starter Kit makes it easy to add CBMC verification to an existing software project.
Key concepts:
- The Reference Guide describes CBMC and the CBMC tool chain
- CBMC primitives and memory primitives are useful when writing CBMC assumptions and CBMC assertions.
- goto programs are the intermediate representation of C code used by the CBMC tool chain
- goto-cc (man page) compiles C into the goto program used by CBMC. It is intended to be a drop-in replacement for
gcc
and cl
.
- goto-instrument (man page) is a collection of tools for modifying goto programs. One example is unwinding loops in a goto program.
- goto-analyser (man page) is a collection of tools for analyzing goto programs. One example is finding the set of reachable functions in a goto program.
Please contribute documentation when you find mistakes or missing information to help us improve this user guide.
Last modified: 2024-12-03 12:50:29 +0000