cprover
CBMC tour
Author
Kareem Khazem

CBMC takes C code or a goto-binary as input and tries to emit traces of executions that lead to crashes or undefined behaviour. The diagram below shows the intermediate steps in this process.

The CProver Manual describes CBMC from a user perspective. Each node in the diagram above links to the appropriate class or module documentation, describing that particular stage in the CBMC pipeline.