EufDPLL

EufDPLL -- A tool to check satisfiability of equality logic formulas. 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.