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. We assume you have installed the tools and have read about proof enough to have passing familiarity with proof, proof harnesses, and building code for proof with CBMC.

• Running cbmc
• Loop unwinding
• Property checking
• Coverage checking
• Proof harnesses
• Proof assumptions
• Goto programs