CBMC projects

This is a short tutorial on how to use CBMC on a software project. We discuss:

• Project planning: How organize your proof, estimate the effort involved, and estimate the return on investment
• Writing a good proof: What does a good proof look like?
• Debugging an error trace: How to debug and repair an issue discovered by CBMC
• Coding for verification: How to write code to make it easy to prove with CBMC
• Proof evaluation: A checklist for proof writers and reviewers to know when a proof is done