The logic of equality with uninterpreted functions (EUF) has been proposed for processor verification. We describe EDPLL, a calculus for proving satisfiability of formulas in this kind of logic. Being based
on the DPLL procedure, EDPLL can adopt heuristics developed for this method.
|Title of host publication||Contributions to the Doctoral Programme of the Second International Joint Conference on Automated Reasoning (IJCAR 2004, Cork, Ireland, July 4-8, 2004)|
|Publication status||Published - 2004|
|Name||CEUR Workshop Proceedings|