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, satisfiability, DPLL procedure