EufDpll - A Tool to Check Satisfiability of Equality Logic Formulas

Olga Tveretina; Wieger Wesselink

doi:10.1016/j.entcs.2008.12.089

EufDpll - A Tool to Check Satisfiability of Equality Logic Formulas

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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.

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	https://doi.org/10.1016/j.entcs.2008.12.089
Publication status	Published - 2009

Keywords

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

Access to Document

10.1016/j.entcs.2008.12.089

Cite this

@inproceedings{c7c90226f13448cb86c4da4c2dd37af0,

title = "EufDpll - A Tool to Check Satisfiability of Equality Logic Formulas",

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.",

keywords = "Equality logic with uninterpreted functions, satisﬁability, DPLL procedure",

author = "Olga Tveretina and Wieger Wesselink",

year = "2009",

doi = "10.1016/j.entcs.2008.12.089",

language = "English",

volume = "225",

pages = "405--420",

booktitle = "Procs of the Irish Conference on the Mathematical Foundations of Computer Science and Information Technology",

publisher = "Electronic Notes in Theoretical Computer Science",

}

EufDpll - A Tool to Check Satisfiability of Equality Logic Formulas. / Tveretina, Olga; Wesselink, Wieger.
Procs of the Irish Conference on the Mathematical Foundations of Computer Science and Information Technology . Vol. 225 Electronic Notes in Theoretical Computer Science, 2009. p. 405-420.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - EufDpll - A Tool to Check Satisfiability of Equality Logic Formulas

AU - Tveretina, Olga

AU - Wesselink, Wieger

PY - 2009

Y1 - 2009

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

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

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

UR - http://www.scopus.com/inward/record.url?scp=58149305574&partnerID=8YFLogxK

U2 - 10.1016/j.entcs.2008.12.089

DO - 10.1016/j.entcs.2008.12.089

M3 - Conference contribution

AN - SCOPUS:58149305574

VL - 225

SP - 405

EP - 420

BT - Procs of the Irish Conference on the Mathematical Foundations of Computer Science and Information Technology

PB - Electronic Notes in Theoretical Computer Science

ER -

EufDpll - A Tool to Check Satisfiability of Equality Logic Formulas

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this