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. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Van De Pol, J., & Tveretina, O. (2005). A BDD-representation for the logic of equality and uninterpreted functions. In Lecture Notes in Computer Science (Vol. 3618, pp. 769–780). Springer Verlag. https://doi.org/10.1007/11549345_66
Mendeley helps you to discover research relevant for your work.