Theory Refinement [experimental]

HiFrog with Theory Refinement:
The right choice of a domain-specific constraint language enables automated verifiers to scale up to large problems.
Satisfiability modulo theories (SMT) solvers implement efficient decision procedures for the constraint languages, but fall short on built-in support for choosing a constraint language which is expressive enough to model a given program.
The theory refinement approach is our experimental feature on HiFrog that enables abstraction refinement directly guided by programs, and builds on the core SMT concept of theories.
The approach has been implemented in the OpenSMT2 SMT solver to leverage bit-precise verification of programs with non-linear arithmetic.
The implementation uses an augmented version of the theory of uninterpreted functions and is capable of directly injecting non-clausal refinements to the inherent Boolean structure of SMT.
Our prototype implementation is available below as a virtual machine containing both the binaries and the benchmark set.  The prototype is competitive with the widely used propositional flattening approach and is several orders of magnitudes faster on some of our benchmark instances.
 
Supplementary material for SAT 2017 paper:
Here everything is provided to reproduce the experimentation results of HiFrog with Theory Refinement published in SAT'17 paper:
 
Downloads:
  • A virtual machine containing the runnable system; if password needed, it is “hifrog”
  • Preliminary evaluation reports are available here.
  • Benchmarks available here whcih are mostly taken from SV-COMP16 and SV-COMP15.

 

Compiling HiFrog for theory Refinement:

1. First, install OpenSMT2 as a library to be used in HiFrog binary; configure & install OpenSMT2 as follows:

OpenSMT2 depends on the following libraries:

  • zlib
  • gmp
  • gmpxx
  • readline
  • flex

Guideline to install the requirements:

sudo apt-get update

sudo apt-get install gcc-6

sudo apt-get install g++-6

sudo rm /usr/bin/cpp /usr/bin/gcc /usr/bin/g++

sudo ln -s /usr/bin/cpp-6 /usr/bin/cpp

sudo ln -s /usr/bin/gcc-6 /usr/bin/gcc

sudo ln -s /usr/bin/g++-6 /usr/bin/g++

sudo apt-get install libtool

sudo apt-get install bison flex

sudo apt-get install autoconf

sudo apt-get install git-all

 

Guideline to Install GMP:

wget ftp://ftp.gmplib.org/pub/gmp/gmp-6.1.2.tar.xz

tar Jxvf gmp-6.1.2.tar.xz

cd gmp-6.1.2

./configure --enable-cxx

make

make check

sudo make install

2. Compile OpenSMT2 for theory refinement as in the following:

$ git clone -b opensmt_SAT2017 https://scm.ti-edu.ch/repogit/opensmt2.git

Enter the opsntm2 folder and run the configure script:

$ cd opensmt2
$ autoreconf --force --install
$ ./configure

Then run make and install.

$ make
$ sudo make install

3. Download HiFrog:

​  $ git clone -b Theoref_SAT2017 https://scm.ti-edu.ch/repogit/hifrog

4. Compile Cprover framework in HiFrog repository:

   $ cd hifrog/trunk/cprover/src; make clean; make
4. Compile HiFrog. 
   $ cd funfrog; make clean; make -f Makefile-no-itp

A small hint: During the compilation, if you happen to see such message "make: *** No rule to make target `../cpp/cpp.a', needed by `hifrog'. Stop.", please do "make" in the mentioned directory. Then again do make in funfrog directory.

Run HiFrog to use theory refinement algorithm.

./hifrog --theoref --bitwidth <n> --heuristic <n> --unwind <n> --claim <n> --custom <ids> <your code-to-verify>

./hifrog --theoref --bitwidth 32 --unwind 10 --heuristic 4 --claim 1 filename.c



You may read on the parameters: heuristic, unwind, claim and custom on ./hifrog --help

 

** If you need any assistance, please contact us **

sepideh.a65[at]gmail.com