UpProver is a Bounded Model Checker that incrementally verifies different revisions of a C program. The key idea in UpProver is reusing efforts from one verification run to another, instead of verifying the full program over and over again. It uses Function Summarization based on Craig interpolation. For both satisfiability solving and interpolation, UpProver uses the SMT solver OpenSMT which is equipped with a flexible interpolation framework for EUF and LRA for computing function summaries. UpProver is implemented in C++. It allows verifying user-specified assertions within a predefined bound.
Project page: http://verify.inf.usi.ch/upprover
First, compile OpenSMT2 (branch master the tag sri-summer-school) as a library and
install it in your system by simply running
$ mkdir build; cd build; cmake ..; make install
Then compile UpProver (uses cmake as a build system generator) using the following command
$ cd upprover/trunk/cprover; mkdir build; cd build; cmake ..; make
The default build type is RELEASE. Different build types can be configured using cmake variable CMAKE_BUILD_TYPE. For example, to create a debug build use
$ cmake -DCMAKE_BUILD_TYPE=Debug ..
To see all the commands, type ./upprover --help.
Check the manual to use UpProver for verifying different revisions of a C program.
If you have questions please mail them to me at [email protected], or to the discussion forum!