Experimentation [FMCAD 2020]

Here everything is provided to reproduce the experimentation results of UpProver for FMCAD 2020 paper:

Installation:

1- Compile and install OpenSMT2 as a library to be used in UpProver:

git clone https://github.com/usi-verification-and-security/opensmt.git
git checkout tags/fmcad2020

 

Then follow the compilation instructions here.

2- Compile UpProver by switching to the UpProver branch:

$ git clone --single-branch --branch upprover https://github.com/usi-verification-and-security/upprover.git
git checkout tags/fmcad2020
cd hifrog/trunk/cprover;
mkdir build;
cd build; 
cmake ..;
make

 

Benchmarks:

Benchmarks used for evaluation of FMCAD2020 submission are available here (mostly from Linux Device Drivers and some challenging hand-crafted benchmarks).

The experiments were run on a CentOS 7.5 x86_64 system with two Intel Xeon E5-2650 CPUs, clocked at 2.30GHz.  and 20 (2 x 10) cores, using a 30 GB memory limit per process and a 600 s timeout on CPU time.

 

Results:

The comparison results of UpProver and eVolCheck are available here. 

The comparison results of UpProver and Precision reuse technique in CPAchecker are available here. 

Note that this performance comparison is indirect as the underlying techniques in the tools are orthogonal, i.e., UpProver is a bounded model checker and CPAchecker is an unbounded verifier.