CBMC
User Guide

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