# CBMC proofs

This chapter goes into greater detail on how to use CBMC on
more realistic examples.

We assume that you are familiar with using CBMC
on [simple examples](debugging.md).
We assume you have [installed the tools](../../installation.md)
and have [read about proof](proof.md) enough to have passing familiarity
with proof, proof harnesses, and building code for proof with CBMC.

* [Running cbmc](cbmc.md)
* [Loop unwinding](loop-unwinding.md)
* [Property checking](checking-properties.md)
* [Coverage checking](checking-coverage.md)
* [Proof harnesses](proof-harnesses.md)
* [Proof assumptions](proof-assumptions.md)
* [Goto programs](goto-programs.md)