Lattice-based SMT for program verification
Proceedings of the 17th ACM-IEEE International Conference on Formal Methods and Models for System Design, pp. 162019.
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...More
Full Text (Upload PDF)
PPT (Upload PPT)