• PRISM

  • Referenced in 454 articles [sw01186]
  • three model checking engines: one symbolic, using BDDs (binary decision diagrams) and MTBDDs (multi-terminal ... BDDs); one based on sparse matrices; and one which combines both symbolic and sparse matrix...
  • NuSMV

  • Referenced in 314 articles [sw04131]
  • first model checker based on BDDs. NuSMV has been designed to be an open architecture...
  • CUDD

  • Referenced in 158 articles [sw04446]
  • provides functions to manipulate Binary Decision Diagrams (BDDs) [5,3], Algebraic Decision Diagrams (ADDs ... Zero-suppressed Binary Decision Diagrams (ZDDs) [12]. BDDs are used to represent switching functions; ADDs ... 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...
  • Bebop

  • Referenced in 73 articles [sw08928]
  • explicitly, and sets of states implicitly using BDDs. By harnessing the inherent modularity in procedural...
  • Rabbit

  • Referenced in 24 articles [sw01317]
  • structure BDD. Good variable orderings for the BDDs are computed from the modular structure...
  • azove

  • Referenced in 13 articles [sw04634]
  • threshold BDDs and the optimal variable ordering problem Many combinatorial optimization problems can be formulated ... accomplished using binary decision diagrams (BDDs), a very popular and effective datastructure in computational logics ... parallel AND operation on threshold BDDs. In particular our algorithm is capable of solving knapsack ... problems and multidimensional knapsack problems. par BDDs are represented as a directed acyclic graph...
  • BuDDy

  • Referenced in 23 articles [sw05791]
  • simple introduction to Binary Decision Diagrams (BDDs) to a full blown BDD package with...
  • SIGREF

  • Referenced in 15 articles [sw00859]
  • bisimulations. Our approach is implemented symbolically using BDDs, which enables the handling of very large...
  • CirCUs

  • Referenced in 9 articles [sw00128]
  • Form (CNF) clauses, and Binary Decision Diagrams (BDDs). We show how BDDs are used ... clauses, enhanced with information extracted from the BDDs. We also describe a new decision variable...
  • SBSAT

  • Referenced in 10 articles [sw00828]
  • sets of arbitrary boolean constraints, represented as BDDs. The approach preprocesses the BDDs into state...
  • FORCE

  • Referenced in 9 articles [sw09016]
  • successfully reduce the size of BDDs and accelerate SAT-solving. Applications to reachability analysis have...
  • BDDNOW

  • Referenced in 6 articles [sw08898]
  • BDDNOW: A Parallel BDD Package. BDDs (binary decision diagrams) are ubiquitous in formal verification tools ... researchers have investigated using parallel processing for BDDs. In this paper, we present a parallel...
  • SMCDEL

  • Referenced in 8 articles [sw29077]
  • which are represented as Binary Decision Diagrams (BDDs). You can try SMCDEL online here...
  • FIREMAN

  • Referenced in 7 articles [sw10594]
  • modeling firewall rules using binary decision diagrams (BDDs), which have been used successfully in hardware...
  • BOXES

  • Referenced in 6 articles [sw21178]
  • weds the strengths of Binary Decision Diagrams (BDDs) and Box. The complexity of the operations...
  • Salsa

  • Referenced in 5 articles [sw25430]
  • Sims, S.: Salsa: Combining constraint solvers with BDDs for automated invariant checking. Salsa...
  • Meddly

  • Referenced in 4 articles [sw29140]
  • supports various types of decision diagrams, including BDDs, MDDs, MTMDDs, EV+MDDs, and EV*MDDs...
  • GBDD

  • Referenced in 1 article [sw15451]
  • GBDD — A package for representing relations with BDDs. Regular Model Checking is a framework ... packages, licensed under GPL: Meta package for BDDs. The package gbdd implements an abstraction layer ... BDDs. This allows several BDD implementation to be used under...
  • JDD

  • Referenced in 1 article [sw41642]
  • just ZDD). Binary Decision Diagrams (BDDs) are used in formal verification, CSP, optimisation and more ... work with BDDs, you need a BDD library. JDD is my java implementation ... also includes support for Zero-suppressed BDDs...
  • Boom

  • Referenced in 2 articles [sw01318]
  • concurrent version of Boom is implemented using BDDs and includes partial order reduction methods. Boom...