Want to apply your solver to software verification problems? Got software you want to verify? Want to work on verification but don't have the time to build all of the infrastructure? Curious to know how program analysers work? This tutorial can help!
We will give an introduction to the CPROVER program verification system, one of the largest, most established and powerful automatic verification systems for C and C++. This will include hands-on sessions with CBMC and information on how to use and integrate CPROVER components in your own systems.
We have three progressively more ambitious goals:
If you are on *NIX and you want to build from source:
git clone https://github.com/diffblue/cbmc cd cbmc/src git checkout cbmc-5.5 make minisat2-download make
Attention: Windows users, please carefully follow the instructions at http://www.cprover.org/cbmc/ to install CBMC before you come to the tutorial.
Either get from GIT:
git clone https://github.com/diffblue/cbmc cbmc-5.4-incremental cd cbmc-5.4-incremental/src git checkout peter-incremental-unwinding make minisat2-download make
or download binary
Either get from GIT:
git clone https://github.com/diffblue/2ls cd 2ls ./install.sh
or download binary
Also see 2LS
Slides
Example Files:
Exercises:
CBMC:
Incremental CBMC:
2LS: