EufDpll - A tool to check satisfiability of equality logic formulas

O. Tveretina, J.W. Wesselink

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

1 Citation (Scopus)


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 languageEnglish
Title of host publicationProceedings of the Irish Conference on the Mathematical Foundations of Computer Science and Information Technology (MFCSIT 2006, Cork, Ireland, August 1-5, 2006)
EditorsA. Seda, M. Boubekeur, T. Hurley, M. Mac an Airchinnigh, M. Schellekens, G. Strong
Publication statusPublished - 2009

Publication series

NameElectronic Notes in Theoretical Computer Science
ISSN (Print)1571-0061


Dive into the research topics of 'EufDpll - A tool to check satisfiability of equality logic formulas'. Together they form a unique fingerprint.

Cite this