EufDpll - A tool to check satisfiability of equality logic formulas

O. Tveretina; J.W. Wesselink

doi:10.1016/j.entcs.2008.12.089

EufDpll - A tool to check satisfiability of equality logic formulas

O. Tveretina, J.W. Wesselink

Formal System Analysis

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

1 Citation (Scopus)

Abstract

Decision procedures for subsets of First-Order Logic form the core of many verification tools. Applications include hardware and software verification. The logic of Equality with Uninterpreted Functions (EUF) is a decidable subset of First-Order Logic. The EUF logic and its extensions have been applied for proving equivalence between systems. We present a branch and bound decision procedure for EUF logic based on the generalisation of the Davis-Putnam-Loveland-Logemann procedure (EUF-DPLL). EufDpll is a tool to check satisfiability of EUF formulas based on this procedure.

Original language	English
Title of host publication	Proceedings of the Irish Conference on the Mathematical Foundations of Computer Science and Information Technology (MFCSIT 2006, Cork, Ireland, August 1-5, 2006)
Editors	A. Seda, M. Boubekeur, T. Hurley, M. Mac an Airchinnigh, M. Schellekens, G. Strong
Pages	405-420
DOIs	https://doi.org/10.1016/j.entcs.2008.12.089
Publication status	Published - 2009

Publication series

Name	Electronic Notes in Theoretical Computer Science
Volume	225
ISSN (Print)	1571-0061

Access to Document

10.1016/j.entcs.2008.12.089

Cite this

Tveretina, O., & Wesselink, J. W. (2009). EufDpll - A tool to check satisfiability of equality logic formulas. In A. Seda, M. Boubekeur, T. Hurley, M. Mac an Airchinnigh, M. Schellekens, & G. Strong (Eds.), Proceedings of the Irish Conference on the Mathematical Foundations of Computer Science and Information Technology (MFCSIT 2006, Cork, Ireland, August 1-5, 2006) (pp. 405-420). (Electronic Notes in Theoretical Computer Science; Vol. 225). https://doi.org/10.1016/j.entcs.2008.12.089

Tveretina, O. ; Wesselink, J.W. / EufDpll - A tool to check satisfiability of equality logic formulas. Proceedings of the Irish Conference on the Mathematical Foundations of Computer Science and Information Technology (MFCSIT 2006, Cork, Ireland, August 1-5, 2006). editor / A. Seda ; M. Boubekeur ; T. Hurley ; M. Mac an Airchinnigh ; M. Schellekens ; G. Strong. 2009. pp. 405-420 (Electronic Notes in Theoretical Computer Science).

@inproceedings{7e74e18dbacd4b98b2ad4c1920fae0f9,

title = "EufDpll - A tool to check satisfiability of equality logic formulas",

abstract = "Decision procedures for subsets of First-Order Logic form the core of many verification tools. Applications include hardware and software verification. The logic of Equality with Uninterpreted Functions (EUF) is a decidable subset of First-Order Logic. The EUF logic and its extensions have been applied for proving equivalence between systems. We present a branch and bound decision procedure for EUF logic based on the generalisation of the Davis-Putnam-Loveland-Logemann procedure (EUF-DPLL). EufDpll is a tool to check satisfiability of EUF formulas based on this procedure.",

author = "O. Tveretina and J.W. Wesselink",

year = "2009",

doi = "10.1016/j.entcs.2008.12.089",

language = "English",

series = "Electronic Notes in Theoretical Computer Science",

pages = "405--420",

editor = "A. Seda and M. Boubekeur and T. Hurley and {Mac an Airchinnigh}, M. and M. Schellekens and G. Strong",

booktitle = "Proceedings of the Irish Conference on the Mathematical Foundations of Computer Science and Information Technology (MFCSIT 2006, Cork, Ireland, August 1-5, 2006)",

}

Tveretina, O & Wesselink, JW 2009, EufDpll - A tool to check satisfiability of equality logic formulas. in A Seda, M Boubekeur, T Hurley, M Mac an Airchinnigh, M Schellekens & G Strong (eds), Proceedings of the Irish Conference on the Mathematical Foundations of Computer Science and Information Technology (MFCSIT 2006, Cork, Ireland, August 1-5, 2006). Electronic Notes in Theoretical Computer Science, vol. 225, pp. 405-420. https://doi.org/10.1016/j.entcs.2008.12.089

EufDpll - A tool to check satisfiability of equality logic formulas. / Tveretina, O.; Wesselink, J.W.
Proceedings of the Irish Conference on the Mathematical Foundations of Computer Science and Information Technology (MFCSIT 2006, Cork, Ireland, August 1-5, 2006). ed. / A. Seda; M. Boubekeur; T. Hurley; M. Mac an Airchinnigh; M. Schellekens; G. Strong. 2009. p. 405-420 (Electronic Notes in Theoretical Computer Science; Vol. 225).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - EufDpll - A tool to check satisfiability of equality logic formulas

AU - Tveretina, O.

AU - Wesselink, J.W.

PY - 2009

Y1 - 2009

N2 - Decision procedures for subsets of First-Order Logic form the core of many verification tools. Applications include hardware and software verification. The logic of Equality with Uninterpreted Functions (EUF) is a decidable subset of First-Order Logic. The EUF logic and its extensions have been applied for proving equivalence between systems. We present a branch and bound decision procedure for EUF logic based on the generalisation of the Davis-Putnam-Loveland-Logemann procedure (EUF-DPLL). EufDpll is a tool to check satisfiability of EUF formulas based on this procedure.

AB - Decision procedures for subsets of First-Order Logic form the core of many verification tools. Applications include hardware and software verification. The logic of Equality with Uninterpreted Functions (EUF) is a decidable subset of First-Order Logic. The EUF logic and its extensions have been applied for proving equivalence between systems. We present a branch and bound decision procedure for EUF logic based on the generalisation of the Davis-Putnam-Loveland-Logemann procedure (EUF-DPLL). EufDpll is a tool to check satisfiability of EUF formulas based on this procedure.

U2 - 10.1016/j.entcs.2008.12.089

DO - 10.1016/j.entcs.2008.12.089

M3 - Conference contribution

T3 - Electronic Notes in Theoretical Computer Science

SP - 405

EP - 420

BT - Proceedings of the Irish Conference on the Mathematical Foundations of Computer Science and Information Technology (MFCSIT 2006, Cork, Ireland, August 1-5, 2006)

A2 - Seda, A.

A2 - Boubekeur, M.

A2 - Hurley, T.

A2 - Mac an Airchinnigh, M.

A2 - Schellekens, M.

A2 - Strong, G.

ER -

Tveretina O, Wesselink JW. EufDpll - A tool to check satisfiability of equality logic formulas. In Seda A, Boubekeur M, Hurley T, Mac an Airchinnigh M, Schellekens M, Strong G, editors, Proceedings of the Irish Conference on the Mathematical Foundations of Computer Science and Information Technology (MFCSIT 2006, Cork, Ireland, August 1-5, 2006). 2009. p. 405-420. (Electronic Notes in Theoretical Computer Science). doi: 10.1016/j.entcs.2008.12.089

EufDpll - A tool to check satisfiability of equality logic formulas

Abstract

Publication series

Access to Document

Fingerprint

Cite this