EufDpll - A Tool to Check Satisfiability of Equality Logic Formulas

Olga Tveretina, Wieger Wesselink

    Research output: Chapter in Book/Report/Conference proceedingConference contribution


    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 languageEnglish
    Title of host publicationProcs of the Irish Conference on the Mathematical Foundations of Computer Science and Information Technology
    PublisherElectronic Notes in Theoretical Computer Science
    Publication statusPublished - 2009


    • Equality logic with uninterpreted functions, satisfiability, DPLL procedure


    Dive into the research topics of 'EufDpll - A Tool to Check Satisfiability of Equality Logic Formulas'. Together they form a unique fingerprint.

    Cite this