# 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.

## References in zbMATH (referenced in 2 articles )

Showing results 1 to 2 of 2.

Sorted by year (- Tveretina, Olga; Wesselink, Wieger: Eufdpll - A tool to check satisfiability of equality logic formulas. (2009)
- Tveretina, Olga; Wesselink, Wieger: EufDPLL -- a tool to check satisfiability of equality logic formulas (2008)