Summary and Theory transformation [experimental]

HiFrog with Summary transformation: 
In this prototype, we implemented a novel SMT-based algorithm for incrementally verifying industrial-size programs with multiple properties. The 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, and the global refinement. In the first stage, it iteratively refines the function summaries 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 summaries. The function summary over-aproximates the concrete representation of the function and can substitute the function body. If during the 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.
 
Supplementary material of LPAR 2018 paper:
Here everything is provided to reproduce the experimentation results of LPAR 2018 paper:
 
  • Preliminary evaluation reports are available here.
  • Benchmarks available here whcih are mostly taken from SV-COMP16 and SV-COMP15.
 
The experiment has been run based on the following setups:

Installation:

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

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

To compile OpenSMT2 simply do the following:

        $ git clone --branch lpar18 $ https://github.com/usi-verification-and-security/opensmt.git --single-branch
        $ cd opensmt2 && mkdir build && cd build
        $ cmake -DPRODUCE_PROOF=ON -DCMAKE_BUILD_TYPE=Release ..
        $ make
        $ make install

2. Compile hifrog source code:

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

$ 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

 

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

sepideh.a65[at]gmail.com