Show simple item record

dc.contributor.authorVakili, Amirhossein
dc.contributor.authorDay, Nancy A. 19:00:33 (GMT) 19:00:33 (GMT)
dc.descriptionThis 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:
dc.description.abstractThe 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.en
dc.subjectfinite model findingen
dc.subjectequality with uninterpreted functionsen
dc.subjectfinite scopeen
dc.subjectsymmetry breaking predicatesen
dc.titleFinite Model Finding Using the Logic of Equality with Uninterpreted Functionsen
dc.typeConference Paperen
dcterms.bibliographicCitationVakili A., Day N.A. (2016) Finite Model Finding Using the Logic of Equality with Uninterpreted Functions. In: Fitzgerald J., Heitmeyer C., Gnesi S., Philippou A. (eds) FM 2016: Formal Methods. FM 2016. Lecture Notes in Computer Science, vol 9995. Springer, Chamen
uws.contributor.affiliation1Faculty of Mathematicsen
uws.contributor.affiliation2David R. Cheriton School of Computer Scienceen

Files in this item


This item appears in the following Collection(s)

Show simple item record


University of Waterloo Library
200 University Avenue West
Waterloo, Ontario, Canada N2L 3G1
519 888 4883

All items in UWSpace are protected by copyright, with all rights reserved.

DSpace software

Service outages