The CUDD package provides functions to manipulate Binary Decision Diagrams (BDDs) [5,3], Algebraic Decision Diagrams (ADDs) , and Zero-suppressed Binary Decision Diagrams (ZDDs) . BDDs are used to represent switching functions; ADDs are used to represent function from to an arbitrary set. ZDDs represent switching functions like BDDs; however, they are much more efficient than BDDs when the functions to be represented are characteristic functions of cube sets, or in general, when the ON-set of the function to be represented is very sparse. They are inferior to BDDs in other cases. The package provides a large set of operations on BDDs, ADDs, and ZDDs, functions to convert BDDs into ADDs or ZDDs and vice versa, and a large assortment of variable reordering methods.
Keywords for this software
References in zbMATH (referenced in 148 articles )
Showing results 141 to 148 of 148.
- Yavuz-Kahveci, Tuba; Tuncer, Murat; Bultan, Tevfik: A library for composite symbolic representations (2001)
- Chatalic, Philippe; Simon, Laurent: ZRes: The old Davis-Putnam procedure meets ZBDD (2000)
- Cimatti, Alessandro; Clarke, Edmund; Giunchiglia, Fausto; Roveri, Marco: NuSMV: A new symbolic model checker (2000)
- Coarfa, Cristian; Demopoulos, Demetrios D.; San Miguel Aguirre, Alfonso; Subramanian, Devika; Vardi, Moshe Y.: Random 3-SAT: The plot thickens (2000)
- de Alfaro, Luca; Kwiatkowska, Marta; Norman, Gethin; Parker, David; Segala, Roberto: Symbolic model checking of probabilistic processes using MTBDDs and the Kronecker representation (2000)
- Fraer, Ranan; Kamhi, Gila; Ziv, Barukh; Vardi, Moshe Y.; Fix, Limor: Prioritized traversal: Efficient reachability analysis for verification and falsification (2000)
- Lind-Nielsen, Jørn; Andersen, Henrik Reif: Stepwise CTL model checking of state/event systems (1999)
- Meinel, Ch.; Slobodová, A.: A reducibility concept for problems defined in terms of ordered binary decision diagrams (1997)
Further publications can be found at: http://vlsi.colorado.edu/~fabio/CUDD/node7.html