@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)",

}