Home

The C Bounded Model Checker (CBMC) is a bounded model checker for C code. This wiki describes how to install CBMC, how to use a CBMC starter kit that makes it easy to write proofs, and how to learn to write CBMC proofs.

• Installation of CBMC and CBMC viewer
• CBMC starter kit manual
  • Installation of the starter kit
    • setup.py
    • setup-proof.py
    • Makefile.common
    • Makefile-project-defines
    • Makefile-project-targets
    • litani manual
  • Writing proofs with the starter kit
    • Makefile
      • Proof harness
  • Running proofs with the starter kit
    • run-cbmc-proofs.py
• CBMC tutorial
  • Simple proofs
  • Proof harnesses
  • Function contracts
  • Function contract tutorial
• CBMC training
  • Plan your proof: How organize your proof, estimate the effort involved, and estimate 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
• Contributors to this project