
PRISM
 Referenced in 454 articles
[sw01186]
 three model checking engines: one symbolic, using BDDs (binary decision diagrams) and MTBDDs (multiterminal ... 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 ... Zerosuppressed 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 SATsolving. 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 Zerosuppressed BDDs...

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