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

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 language | English |
---|---|

Title of host publication | Procs of the Irish Conference on the Mathematical Foundations of Computer Science and Information Technology |

Publisher | Electronic Notes in Theoretical Computer Science |

Pages | 405-420 |

Volume | 225 |

DOIs | |

Publication status | Published - 2009 |

## Keywords

- Equality logic with uninterpreted functions, satisﬁability, DPLL procedure