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

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

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

    1 Citation (Scopus)
    2 Downloads (Pure)

    Abstract

    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.
    Original languageEnglish
    Title of host publicationMathematical foundations of computer science : 30th international symposium, MFCS 2005, Gdansk, Poland, August 29-September 2, 2005 : proceedings
    EditorsJ. Jedrzejowicz, A. Szepietowski
    Place of PublicationBerlin
    PublisherSpringer
    Pages769-780
    ISBN (Print)3-540-28702-7
    DOIs
    Publication statusPublished - 2005

    Publication series

    NameLecture Notes in Computer Science
    Volume3618
    ISSN (Print)0302-9743

    Fingerprint

    Dive into the research topics of 'A BDD-representation for the logic of equality and uninterpreted functions'. Together they form a unique fingerprint.

    Cite this