cbmc

Learning

• Material for AWS training days: https://github.com/diffblue/aws-training/tree/main
• http://www.cprover.org/cprover-manual/cbmc/tutorial/
• https://model-checking.github.io/cbmc-training/
• CBMC Manual, https://www.cprover.org/cbmc/doc/manual.pdf

Success stories

• Verification challenge:
  • Stupid RCU Tricks: rcutorture Catches an RCU Bug
  • Verification Challenge 2: RCU NO_HZ_FULL_SYSIDLE
  • Verification Challenge 3: cbmc
• Model checking boot code from AWS data centers, PDF
• Using model checking tools to triage the severity of security bugs in the Xen hypervisor
• Formally Verifying the Correctness and Safety of OpenTitan Boot Code using CBMC, PDF

Tools

• cbmc-viewer
• https://github.com/model-checking/cbmc-proof-debugger