DPLL-based procedure for equality logic with uninterpreted functions

O. Tveretina

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    Abstract

    The logic of equality with uninterpreted functions (EUF) has been proposed for processor verification. We describe EDPLL, a calculus for proving satisfiability of formulas in this kind of logic. Being based on the DPLL procedure, EDPLL can adopt heuristics developed for this method.
    Original languageEnglish
    Title of host publicationContributions to the Doctoral Programme of the Second International Joint Conference on Automated Reasoning (IJCAR 2004, Cork, Ireland, July 4-8, 2004)
    EditorsU. Sattler
    Publication statusPublished - 2004

    Publication series

    NameCEUR Workshop Proceedings
    Volume14
    ISSN (Print)1613-0073

    Cite this