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.
|Title of host publication||Mathematical foundations of computer science : 30th international symposium, MFCS 2005, Gdansk, Poland, August 29-September 2, 2005 : proceedings|
|Editors||J. Jedrzejowicz, A. Szepietowski|
|Place of Publication||Berlin|
|Publication status||Published - 2005|
|Name||Lecture Notes in Computer Science|