Finite Model Finding Using the Logic of Equality with Uninterpreted Functions
FM, pp. 677-693, 2016.
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 wit...More
Full Text (Upload PDF)
PPT (Upload PPT)