User Guide

For a quick start with CBMC on simple problems, read

• The Installation Guide
• A short tutorial
• A short manual

For a quick start with CBMC on large software projects, read

• Deploying CBMC on industrial software projects describing how to use CBMC as part of routine software development and continuous integration.

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-11-20 06:00:32 -0800