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  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  (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.
 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]
 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:
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.
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 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.