Lattice-based SMT for Program Verification

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

Research output: Chapter in Book/Report/Conference proceedingConference paperpeer-review

285 Downloads (Pure)

Abstract

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.
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
PublisherACM
Pages1-11
ISBN (Electronic)9781450369978
DOIs
Publication statusPublished - 9 Oct 2019

Fingerprint

Dive into the research topics of 'Lattice-based SMT for Program Verification'. Together they form a unique fingerprint.

Cite this