King's College London

Research portal

Lattice-based SMT for Program Verification

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Karine Even Mendoza, Antti Hyyvarinen, Hana Chockler, Natasha Sharygina

Original languageEnglish
Title of host publicationMEMOCODE 2019 - 17th ACM-IEEE International Conference on Formal Methods and Models for System Design
Subtitle of host publication17th ACM-IEEE International Conference on Formal Methods and Models for System Design
ISBN (Electronic)9781450369978
Publication statusPublished - 9 Oct 2019


King's Authors


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.

Our lightweight theory uses lattices for efficient representation of library functions by a subset of guarded literals. These lattices are constructed from equations and inequalities of properties of the library functions. These subsets are found during the lattice traversal. We generalise the method to a number of lattices for functions whose values depend on each other in the program, and we describe a simultaneous traversal algorithm of several lattices, so that a combination of guarded literals from all lattices does not lead to contradictory values of their variables.

We evaluate our approach on benchmarks taken from the robotics community, and our experimental results demonstrate that we are able to solve a number of instances that were previously unsolvable by existing SMT solvers.

Download statistics

No data available

View graph of relations

© 2018 King's College London | Strand | London WC2R 2LS | England | United Kingdom | Tel +44 (0)20 7836 5454