The CPROVER Manual

1. Introduction
2. Installation
3. CBMC – Bounded Model Checking
   • A Short Tutorial
   • Loop Unwinding
   • Assertion Checking
4. Compositional Reasoning using Code Contracts
5. Goto-Analyzer – Abstract Interpretation
6. Test Suite Generation
7. Program Properties
8. Modeling
   • Nondeterminism
   • Assumptions
   • Pointers
   • Floating Point
   • Generating Environments
9. Build Systems
   • Integration into Build Systems with goto-cc
   • Integration with Visual Studio builds
10. The CPROVER API Reference

Last modified: 2022-09-29 15:10:20 -0400