DPLL-based procedure for equality logic with uninterpreted functions

O. Tveretina

    Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

    Samenvatting

    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.
    Originele taal-2Engels
    TitelContributions to the Doctoral Programme of the Second International Joint Conference on Automated Reasoning (IJCAR 2004, Cork, Ireland, July 4-8, 2004)
    RedacteurenU. Sattler
    StatusGepubliceerd - 2004

    Publicatie series

    NaamCEUR Workshop Proceedings
    Volume14
    ISSN van geprinte versie1613-0073

    Vingerafdruk

    Duik in de onderzoeksthema's van 'DPLL-based procedure for equality logic with uninterpreted functions'. Samen vormen ze een unieke vingerafdruk.

    Citeer dit