Skip to content


Folders and files

Last commit message
Last commit date

Latest commit


Repository files navigation



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:


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

Changing build type

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, or to the discussion forum!