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
• Install the CBMC starter kit
• Plan your proof
• Write a good proof
• Debug an error trace
• Code for verification
• Code review for proofs
• Frequently Asked Questions

Many people have contributed to this work:

• Contributors