Skip to content

Latest commit

 

History

History
30 lines (21 loc) · 959 Bytes

developer_guide.md

File metadata and controls

30 lines (21 loc) · 959 Bytes

\page developer_guide Developer Guide

For a quick start on developing for CBMC, read

  • A \ref tutorial "short developer tutorial"

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

  • \ref cprover_documentation

Key concepts:

  • \ref compilation-and-development "Compiling and developing" for CBMC
  • \ref background-concepts "Background concepts" including ASTs, CFGs, and SSA, bounded model checking, and static analysis
  • \ref goto-programs "Goto programs"
  • \ref goto-symex "Symbolic execution"
  • \ref solvers "Decision procedures"
  • \ref folder-walkthrough "Code organization"
  • CPROVER primitives

Miscellaneous documentation:

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