The CUDD package provides functions to manipulate Binary Decision Diagrams (BDDs) [5,3], Algebraic Decision Diagrams (ADDs) [1], and Zero-suppressed Binary Decision Diagrams (ZDDs) [12]. 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.

References in zbMATH (referenced in 116 articles )

Showing results 1 to 20 of 116.
Sorted by year (citations)

1 2 3 4 5 6 next

  1. Abujarad, Fuad; Lin, Yiyan; Bonakdarpour, Borzoo; Kulkarni, Sandeep S.: The complexity of automated addition of fault-tolerance without explicit legitimate states (2015)
  2. Ghosh, Kamalesh; Dasgupta, Pallab; Ramesh, S.: Automated planning as an early verification tool for distributed control (2015)
  3. Pang, Tao; Duan, Zhenhua; Liu, Xiaofang: A symbolic model checker for propositional projection temporal logic (2015)
  4. Bollig, Beate: A simpler counterexample to a long-standing conjecture on the complexity of Bryant’s apply algorithm (2014)
  5. Brickenstein, Michael; Dreyer, Alexander: Gröbner-free normal forms for Boolean polynomials (2013)
  6. Cau, Antonio; Janicke, Helge; Moszkowski, Ben: Verification and enforcement of access control policies (2013)
  7. Chatterjee, Krishnendu; Henzinger, Monika; Joglekar, Manas; Shah, Nisarg: Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives (2013)
  8. Gordon, Andrew D.; Aizatulin, Mihhail; Borgstrom, Johannes; Claret, Guillaume; Graepel, Thore; Nori, Aditya V.; Rajamani, Sriram K.; Russo, Claudio: A model-learner pattern for Bayesian reasoning (2013)
  9. Aarts, Fides; Heidarian, Faranak; Kuppens, Harco; Olsen, Petur; Vaandrager, Frits: Automata learning through counterexample guided abstraction refinement (2012)
  10. Berghammer, Rudolf; Bolus, Stefan: On the use of binary decision diagrams for solving problems on simple games (2012)
  11. Bloem, Roderick; Jobstmann, Barbara; Piterman, Nir; Pnueli, Amir; Sa’ar, Yaniv: Synthesis of Reactive(1) designs (2012)
  12. Damm, Werner; Dierks, Henning; Disch, Stefan; Hagemann, Willem; Pigorsch, Florian; Scholl, Christoph; Waldmann, Uwe; Wirtz, Boris: Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces (2012)
  13. Ehlers, Rüdiger: Symbolic bounded synthesis (2012)
  14. Lengál, Ondřej; Šimáček, Jiří; Vojnar, Tomáš: VATA: A library for efficient manipulation of non-deterministic tree automata (2012)
  15. Lomuscio, Alessio; Penczek, Wojciech: Symbolic model checking for temporal-epistemic logic (2012)
  16. Yoshinaka, Ryo; Kawahara, Jun; Denzumi, Shuhei; Arimura, Hiroki; Minato, Shin-Ichi: Counterexamples to the long-standing conjecture on the complexity of BDD binary operations (2012)
  17. Abujarad, F.; Kulkarni, S.S.: Automated constraint-based addition of nonmasking and stabilizing fault-tolerance (2011)
  18. Bryce, Daniel; Cushing, William; Kambhampati, Subbarao: State agnostic planning graphs: deterministic, non-deterministic, and probabilistic planning (2011)
  19. Cabodi, Gianpiero; Nocco, Sergio; Quer, Stefano: Benchmarking a model checker for algorithmic improvements and tuning for performance (2011)
  20. Holík, Lukáš; Lengál, Ondřej; Šimáček, Jiří; Vojnar, Tomáš: Efficient inclusion checking on explicit and semi-symbolic tree automata (2011)

1 2 3 4 5 6 next

Further publications can be found at: