| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 421916 | Electronic Notes in Theoretical Computer Science | 2009 | 16 Pages |
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
