Summary & Theory Refinement [experimental]

Description of the research idea:
In this prototype, we implemented a novel SMT-based approach to incremental verification scalable to large-scale programs with multiple properties on top of Bounded Model Checker Hifrog.
Our key idea is to exploit both the function summaries and the overall precision of the program encoding lazily. That is, among several theories available for the encoding, we are trying to identify the lightest theory suitable for each given property.
At the moment, the summary and theory refinement algorithm deals with three theories: EUF, LRA, and bit-vectors (using a proposed augmented version in SAT2017).
 
Our algorithm attempts to co-operate both summary and theory refinement on demand; the refinement phase is split into two phases the local refinement stage and the global refinement stage. In the first stage, it iteratively refines the function summary involved in the error trace only. In the second stage, it changes the whole encoding of the program from less precise to more precise. 
 
In the local refinement stage, interpolation-based proof plays a key role to compute function summary. The function summary can substitute the concrete body of the function. If during verification it turns out that the property being checked does not hold, it might be because of function summary was not precise enough to prove the property, thus in such situation local refinement comes into play for refining the function summary for making it more precise.
 
The global refinement stage starts to operate when local refinement was still insufficient to verify the property being checked.  Such situation is compensated by changing the entire encoding of a program from less precise encoding to slightly more precise one, given the fact that there is a set of different SMT encodings with different level of precision.
 
We have implemented the summary and theory refinement algorithm on top of HiFrog, an incremental bounded model checker. As a backend HiFrog uses SMT-solver OpenSMT which is equipped with a flexible interpolation framework for EUF and LRA for computing the function summaries. Technical information about the setup of the tool and evaluation results can be found in the following.
 
The prototype is competitive with CBMC and is several orders of magnitudes faster on some of our benchmark instances.
 
Experimental results:
  • Preliminary evaluation reports are available here. (mostly from SV-COMP16 and SV-COMP15).
  • Benchmarks
 
The experiment has been run based on the following setups:
 

Installation:

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

​​OpenSMT2 depends on the libraries: zlibgmp,gmpxxreadline, flex. If you do not have them installed, please first check installation guide for libraries, then continue the following steps:

To compile OpenSMT2, first download it via:

$ git clone --branch lpar18 https://scm.ti-edu.ch/repogit/opensmt2.git --single-branch   

Enter the opensmt2 folder and create a build directory and enter it:

$ cd opensmt2 && mkdir build && cd build
$ cmake -DPRODUCE_PROOF=ON -DCMAKE_BUILD_TYPE=Release ..

Then compile using make and install the library.

$ make
$ make install

2. Get the git repository of hifrog:

​  $ git clone --branch lpar18 https://scm.ti-edu.ch/repogit/hifrog

3. Create build directory and build hifrog using cmake

   $ cd hifrog/trunk/cprover && mkdir build && cd build
   $ cmake -DCMAKE_BUILD_TYPE=Release ..
   $ make

 

Run HiFrog to use summary & theory refinement algorithm.

./hifrog --sum-theoref --unwind <n> filename.c

 

The git repository we use for HiFrog is hosted at https://scm.ti-edu.ch/projects/hifrog.

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

sepideh.a65[at]gmail.com