The CPROVER Manual

1. Introduction
2. Installation
3. CBMC – Bounded Model Checking
   • A Short Tutorial
   • Loop Unwinding
   • Assertion Checking
4. Goto-Analyzer – Abstract Interpretation
5. Test Suite Generation
6. Program Properties
7. Modeling
   • Nondeterminism
   • Assumptions
   • Pointers
   • Floating Point
   • Generating Environments
   • Memory-mapped I/O
   • Shadow Memory
8. Build Systems
   • Integration into Build Systems with goto-cc
   • Integration with Visual Studio builds
9. The CPROVER API Reference
10. Background Information on selected Command-line Options

• Incremental SMT solver
• Unsound options

Last modified: 2026-01-09 02:17:24 +0100