CBMC: Developer Guide

For a quick start on developing for CBMC, read

• A short developer tutorial

The traditional developer documentation is generated by doxygen from the source code:

• CProver documentation

Key concepts:

• Compiling and developing for CBMC
• Background concepts including ASTs, CFGs, and SSA, bounded model checking, and static analysis
• Goto programs
• Symbolic execution
• Decision procedures
• Code organization
• CPROVER primitives

Miscellaneous documentation:

• CProver Architecture Decision Records
• CProver Assets

Please contribute documentation when you find mistakes or missing information to help us improve this developer guide.

Last modified: 2026年07月02日 20:25:14 +0200