Here everything is provided to reproduce the experimentation results of "HiFrog with lattice refinement" published in VSTTE 2018 and Memocode 2019:
HiFrog with Lattice Refinement:
Lattice-Based Counterexample-Guided Refinement Algorithm offers refinement for Bounded Model Checking with SMT solvers of programs using a library of either standard or user-defined functions.
Typically, if the program correctness depends on the output of a library function, the model-checking process either treats this function as an uninterpreted function, or is required to use a theory under which the function in question is fully defined. The former approach leads to numerous spurious counter-examples, whereas the latter faces the danger of the state-explosion problem, where the resulting formula is too large to be solved by means of modern SMT solvers.
We suggest using a lattice with properties of mathematical functions to model library functions in programs with EUF or extensions of EUF. We present [1] the full details of our lattice-based refinement algorithm and propose an algorithm for constructing a lattice of literals from a set of properties, each of which is encoded into one or more summaries. We present [2] (full version here) the LB-CEGAR algorithm, a full and generalised algorithm of the lattice-based refinement algorithm for programs with multiple different library functions call. The algorithm represents a function efficiently via a lattice of literals (as first-order formulas) and gradually refines the current representation of this function according to the partial order of literals even if we do not have or wish to use the full definition of this function.
[1] Karine Even-Mendoza, Sepideh Asadi, Antti E. J. Hyvärinen, Hana Chockler, Natasha Sharygina: Lattice-Based Refinement in Bounded Model Checking. VSTTE 2018: 50-68. [pdf]
[2] Karine Even-Mendoza, Antti E. J. Hyvärinen, Hana Chockler, Natasha Sharygina: Lattice-based SMT for Program Verification. Accepted to Memocode 2019. [pdf]
Full Proofs and Additional Examples of LB-CEGAR:
- Examples of User-defined Summaries are available here and here.
- Examples of the construction of a lattice of guarded literals are available here and here and here.
- Examples of lattice traversal and additional explanations are available here and here.
- Additional materials and our up-to-date draft describing the techniques are available here and here.
Techniqal Information:
Tools required: HiFrog, OpenSMT, z3
We use Z3 version 4.8 and OpenSMT git/Master version. OpenSMT and HiForg are compiled with Cmake Version 3.5.1.
A Virtual Machine with the tools prototype version is available here with its readme file here.
Note that for the experimental results of the method, we used the Git versions: mod-V1 and trigo-v2. The stable version is available here.
General options for LB-CEGAR in HiFrog:
The Data for the Evaluation of Modulo Function:
- The list of all the lemmas and theorems from the Coq proof assistant to build the modulo lattice are available here.
- The lattices for modulo operation are available here.
- The models and summary files for the experiments are available here.
- The prototype implementation (v1) is available here.
- Verification results of a prototype of the lattice refinement algorithm against other techniques are available here.
- The validation tests are available here and the benchmarks are available here.
- The logs of experimentation are available here.
The Data for the Evaluation of Sine and Cosine Functions:
- General technical information is available here.
- The data-structures are available here.
- The implementation (v2) is available here.
