1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
\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](api/index.html)
Miscellaneous documentation:
* [CProver Architecture Decision Records](adr/index.html)
* [CProver Assets](assets/index.html)
Please \ref contributing_documentation "contribute documentation"
when you find mistakes or missing information to help us improve this
developer guide.
|
