@inproceedings{d7e9816601804ea2827a97e99f05d5cc,

title = "A BDD-representation for the logic of equality and uninterpreted functions",

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.",

author = "{Pol, van de}, J.C. and O. Tveretina",

year = "2005",

doi = "10.1007/11549345_66",

language = "English",

isbn = "3-540-28702-7",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "769--780",

editor = "J. Jedrzejowicz and A. Szepietowski",

booktitle = "Mathematical foundations of computer science : 30th international symposium, MFCS 2005, Gdansk, Poland, August 29-September 2, 2005 : proceedings",

address = "Germany",

}