EufDpll - A Tool to Check Satisfiability of Equality Logic Formulas

Olga Tveretina, Wieger Wesselink

    Research output: Chapter in Book/Report/Conference proceedingConference 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 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
    Pages405-420
    Volume225
    DOIs
    Publication statusPublished - 2009

    Keywords

    • Equality logic with uninterpreted functions, satisfiability, DPLL procedure

    Fingerprint

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

    Cite this