Lattice-based SMT for program verification
Karine Even-Mendoza, Antti E. J. Hyvärinen, Hana Chockler, Natasha Sharygina · 2019
We present a lattice-based satisfiability modulo theory for verification of programs with library functions, for which the mathematical libraries supporting these functions contain a high number of equations and inequalities. Common strategies for dealing with library functions include treating them as uninterpreted functions or using the theories under which the functions are fully defined. The full definition could in most cases lead to instances that are too large to solve efficiently.