dc.contributor.author | Vakili, Amirhossein | |
dc.contributor.author | Day, Nancy A. | |
dc.date.accessioned | 2020-07-06 19:00:33 (GMT) | |
dc.date.available | 2020-07-06 19:00:33 (GMT) | |
dc.date.issued | 2016 | |
dc.identifier.uri | https://dx.doi.org/10.1007/978-3-319-48989-6_41 | |
dc.identifier.uri | http://hdl.handle.net/10012/16034 | |
dc.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 | en |
dc.description.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. | en |
dc.language.iso | en | en |
dc.publisher | Springer | en |
dc.subject | finite model finding | en |
dc.subject | equality with uninterpreted functions | en |
dc.subject | finite scope | en |
dc.subject | kodkod | en |
dc.subject | symmetry breaking predicates | en |
dc.title | Finite Model Finding Using the Logic of Equality with Uninterpreted Functions | en |
dc.type | Conference Paper | en |
dcterms.bibliographicCitation | Vakili 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, Cham | en |
uws.contributor.affiliation1 | Faculty of Mathematics | en |
uws.contributor.affiliation2 | David R. Cheriton School of Computer Science | en |
uws.typeOfResource | Text | en |
uws.peerReviewStatus | Reviewed | en |
uws.scholarLevel | Faculty | en |
uws.scholarLevel | Graduate | en |