Finite Model Finding Using the Logic of Equality with Uninterpreted Functions
Loading...
Date
2016
Authors
Vakili, Amirhossein
Day, Nancy A.
Journal Title
Journal ISSN
Volume Title
Publisher
Springer
Abstract
The problem of finite model finding, finding a satisfying model for a set of first-order logic formulas for a finite scope, is an important step in many verification techniques. In MACE-style solvers, the problem is mapped directly to a SAT problem. We investigate an alternative solution of mapping the problem to the logic of equality with uninterpreted functions (EUF), a decidable logic with many well-supported tools (e.g., SMT solvers). EUF reasoners take advantage of the typed functional structures found in the formulas to improve performance. The challenge is that EUF reasoning is not inherently finite scope. We present an algorithm for mapping a finite model finding problem to an equisatisfiable EUF problem. We present results that show our method has better overall performance than existing tools on a range of problems.
Description
This is a post-peer-review, pre-copyedit version of a paper presented at the International Symposium on Formal Methods. The final authenticated version is available online at: https://dx.doi.org/10.1007/978-3-319-48989-6_41
Keywords
finite model finding, equality with uninterpreted functions, finite scope, kodkod, symmetry breaking predicates