Home | english  | Impressum | Sitemap | KIT

EufDpll - A Tool to Check Satisfiability of Equality Logic Formulas

EufDpll - A Tool to Check Satisfiability of Equality Logic Formulas
Autor:

Olga Tveretina, Wieger Wesselink

Links:
Quelle:

Proceedings of the Irish Conference on the Mathematical Foundations of Computer Science and Information Technology

Electronic Notes in Theoretical Computer Science 225:405-420

Datum: 2009

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.