cprover
/builddir/build/BUILD/cbmc-cbmc-5.8/doc/architectural/front-page.md
Go to the documentation of this file.
1 CProver Documentation
2 =====================
3 
4 \author Kareem Khazem
5 
6 These pages contain user tutorials, automatically-generated API
7 documentation, and higher-level architectural overviews for the
8 CProver codebase. Users can download CProver tools from the
9 <a href="http://www.cprover.org/">CProver website</a>; contributors
10 should use the <a href="https://github.com/diffblue/cbmc">repository</a>
11 hosted on GitHub.
12 
13 ### For users:
14 
15 * The \ref cprover-manual "CProver Manual" details the capabilities of
16  CBMC and SATABS and describes how to install and use these tools. It
17  also covers the underlying theory and prerequisite concepts behind how
18  these tools work.
19 
20 ### For contributors:
21 
22 * If you already know exactly what you're looking for, the API reference
23  is generated from the codebase. You can search for classes and class
24  members in the search bar at top-right or use one of the links in the
25  sidebar.
26 
27 * For higher-level architectural information, each of the pages under
28  the "Modules" link in the sidebar gives an overview of a directory in
29  the CProver codebase.
30 
31 * The \ref module_cbmc "CBMC guided tour" is a good start for new
32  contributors to CBMC. It describes the stages through which CBMC
33  transforms source files into bug reports and counterexamples, linking
34  to the relevant documentation for each stage.
35 
36 * The \subpage cbmc-hacking "CBMC hacking HOWTO" helps new contributors
37  to CProver to get their feet wet through a series of programming
38  exercises---mostly modifying goto-instrument, and thus learning to
39  manipulate the main data structures used within CBMC.
40 
41 * The \subpage cbmc-guide "CBMC guide" is a single document describing
42  the layout of the codebase and many of the important data structures.
43  It probably contains more information than the module pages at the
44  moment, but may be somewhat out-of-date.
45 
46 \defgroup module_hidden _hidden