# Summary

* [CBMC quick start](README.md)
  * [CBMC installation](installation.md)
  * [CBMC as unit testing](cbmc/overview/unit-testing.md)
  * [CBMC as debugging](cbmc/overview/debugging.md)
  * [CBMC as proof](cbmc/overview/proof.md)
* [CBMC proofs](cbmc/overview/README.md)
  * [Running cbmc](cbmc/overview/cbmc.md)
  * [Loop unwinding](cbmc/overview/loop-unwinding.md)
  * [Property checking](cbmc/overview/checking-properties.md)
  * [Coverage checking](cbmc/overview/checking-coverage.md)
  * [Proof harnesses](cbmc/overview/proof-harnesses.md)
  * [Proof assumptions](cbmc/overview/proof-assumptions.md)
  * [Goto programs](cbmc/overview/goto-programs.md)
* [CBMC proof projects](starter-kit/overview/README.md)

* [CBMC viewer]()
* [Litani]()
* [Continuous integration]()

* [Frequently asked questions](faq/README.md)
  * [How does CBMC work?](faq/cbmc.md)
  * [What is loop unwinding?](faq/loop-unwinding.md)
  * [How do memory pointers work?](faq/memory-model.md)
  * [How do function pointers work?]()
  * [How does malloc work?](faq/malloc.md)
  * [How do I write a good stub?]()
  * [What do I do when CBMC won't stop?](faq/termination.md)

* [CBMC project management](management/README.md)
  * [Project planning](management/Plan-your-proof.md)
  * [Writing a good proof](management/Write-a-good-proof.md)
  * [Debugging an error trace](management/Debug-an-error-trace.md)
  * [Coding for verification](management/Code-for-verification.md)
  * [Proof evaluation](management/Code-review-for-proofs.md)

* [CBMC projects](projects.md)

* [CBMC resources](resources.md)