A BDD-representation for the logic of equality and uninterpreted functions

J.C. Pol, van de, O. Tveretina

    Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

    1 Citaat (Scopus)
    2 Downloads (Pure)


    The logic of equality and uninterpreted functions (EUF) has been proposed for processor verification. This paper presents a new data structure called Binary Decision Diagrams for representing EUF formulas (EUF-BDDs). We define EUF-BDDs similar to BDDs, but we allow equalities between terms as labels instead of Boolean variables. We provide an approach to build a reduced ordered EUF-BDD (EUF-ROBDD) and prove that every path to a leaf is satisfiable by construction. Moreover, EUF-ROBDDs are logically equivalent representations of EUF-formulae, so they can also be used to represent state spaces in symbolic model checking with data.
    Originele taal-2Engels
    TitelMathematical foundations of computer science : 30th international symposium, MFCS 2005, Gdansk, Poland, August 29-September 2, 2005 : proceedings
    RedacteurenJ. Jedrzejowicz, A. Szepietowski
    Plaats van productieBerlin
    ISBN van geprinte versie3-540-28702-7
    StatusGepubliceerd - 2005

    Publicatie series

    NaamLecture Notes in Computer Science
    ISSN van geprinte versie0302-9743


    Duik in de onderzoeksthema's van 'A BDD-representation for the logic of equality and uninterpreted functions'. Samen vormen ze een unieke vingerafdruk.

    Citeer dit