Lattice-Based Counterexample-Guided Refinement Algorithm offers a 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 later 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 explainations 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

__; the__

**here****code of HiFrog with a local OpenSMT**version, is available

**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 summaries 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.**