http://www.cprover.org

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:

1. To give people an awareness of what tools we have, what they can and can't do and what are solved problems.
2. To give them the skills they need to use these tools for producing benchmarks, research experiments, verifying their own programs and teaching.
3. To give them the foundations of how to use and integrate components of CPROVER into their own systems.

1. Software verification – what problems are we solving, how do we solve them and what kind of tools are available.
2. Overview of the CPROVER system, components, capabilities, tools.
3. Hands on session: CBMC.
4. CPROVER internals and how to integrate other tools.
5. Advanced topics: concurrency, incremental BMC
6. 2LS: program analysis beyond BMC
7. Hands on session: 2LS.

http://www.cprover.org/cbmc/

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

Linux x86_64 binary

Either get from GIT:

git clone https://github.com/diffblue/2ls
cd 2ls
./install.sh

or download binary

Linux x86_64 binary

Also see 2LS

Slides

tutorial-slides1.pdf

Example Files:

abs.c

escapefunction.c

escapefunctionharness.c

simple.c

Exercises:

loopunwinding.c

sorting.c

searchtree.c

tutorial-slides2.pdf

CBMC:

concurrency1.c

concurrency2.c

concurrency3.c

Incremental CBMC:

incremental.c

2LS:

invariants.c

apache-escape-absolute.c

interprocedural.c

termination.c

Daniel Kroening Martin Brain Peter Schrammel