Home

This is the CBMC Starter Kit, a collection of templates and training material to help you write proofs about C code using the C Bounded Model Checker or CBMC.

• Install CBMC: How to install CBMC and CBMC viewer
• Install the CBMC starter kit: How to install the CBMC starter kit
• Plan your proof: How organize your proof effort and how to estimate the effort involved and the return on investment
• Write a good proof: What does a good proof look like?
• Debug an error trace: How to debug and repair an issue discovered by CBMC
• Code for verification: How to write code to make it easy to prove with CBMC
• Code review for proofs: A checklist for proof writers and reviewers to know when a proof is done
• Frequently Asked Questions

Many people have contributed to this work:

• Contributors