• HOL

  • Referenced in 508 articles [sw05492]
  • external programs such as SAT and BDD engines. HOL 4 is particularly suitable...
  • NuSMV

  • Referenced in 298 articles [sw04131]
  • applied to other research areas. NuSMV2, combines BDD-based model checking component that exploits...
  • Esterel

  • Referenced in 163 articles [sw20012]
  • also provide support for explicit or BDD-based verification tools that perform either bisimulation reduction...
  • MONA

  • Referenced in 122 articles [sw06170]
  • tree automata, three-valued logic, eager minimization, BDD-based automata representations, and cache-conscious data...
  • Rabbit

  • Referenced in 24 articles [sw01317]
  • Rabbit: A tool for BDD-based verification of real-time systems. This paper gives ... checking, both implemented using the data structure BDD. Good variable orderings for the BDDs ... model and an estimate of the BDD size. This leads to a significant performance improvement ... compared to the tool RED and the BDD-based version of Kronos...
  • BuDDy

  • Referenced in 22 articles [sw05791]
  • Decision Diagrams (BDDs) to a full blown BDD package with all the standard BDD operations...
  • MCK

  • Referenced in 30 articles [sw09465]
  • releases of MCK were based primarily on BDD-based model checking algorithms...
  • azove

  • Referenced in 12 articles [sw04634]
  • output-sensitive$ algorithm for building a BDD for a linear constraint (a so-called threshold ... BDD) and a parallel AND operation on threshold BDDs. In particular our algorithm is capable ... directed acyclic graph. The size of a BDD is the number of nodes ... optimal variable ordering of a threshold BDD. This $0/1$ IP formulation provides the basis...
  • LTSmin

  • Referenced in 18 articles [sw07214]
  • symbolic state storage (vector set), fully symbolic (BDD-based) reachability, distributed reachability (MPI-based...
  • MCMAS-SLK

  • Referenced in 17 articles [sw24778]
  • logic specifications. We introduce MCMAS-SLK, a BDD-based model checker for the verification...
  • SIGREF

  • Referenced in 15 articles [sw00859]
  • building blocks, which naturally correspond to efficient BDD operations. Thus, the definition of an appropriate...
  • CVT

  • Referenced in 15 articles [sw09952]
  • uninterpreted functions and their analysis over a BDD-represented small model enables us to validate...
  • MUP

  • Referenced in 15 articles [sw11910]
  • minimal unsatisfiability of any CNF formula through BDD manipulation. This algorithm has a worse-case...
  • SBSAT

  • Referenced in 10 articles [sw00828]
  • SBSAT: a state-based, BDD-based satisfiability solver We present a new approach ... using a tool set similar to standard BDD engines. And it memoizes search information during...
  • DCVALID

  • Referenced in 14 articles [sw20416]
  • MONA which provides efficient multi-terminal BDD based representation of automata and has implemented algorithms...
  • TRANSYT

  • Referenced in 7 articles [sw00976]
  • TRANSYT is a BDD-based tool specifically designed for the verification of timed and untimed ... easily integrated. A state of the art BDD package is integrated into the system ... middleware extension provides support complex BDD manipulation strategies...
  • BDDNOW

  • Referenced in 6 articles [sw08898]
  • BDDNOW: A Parallel BDD Package. BDDs (binary decision diagrams) are ubiquitous in formal verification tools ... time and memory used by the BDD package is frequently the constraint that prevents application ... this paper, we present a parallel BDD package with several novel features. The parallelization scheme ... variable reordering, and simultaneous computation of multiple BDD operations. Finally, the package is designed...
  • fc2tools

  • Referenced in 11 articles [sw12386]
  • combined use of explicit and implicit (BDD) implementation styles for better efficiency; use of specific...
  • Spacer

  • Referenced in 11 articles [sw19496]
  • worst-case bounds of the best BDD-based algorithms. For Linear Arithmetic (integers and rationals...
  • CirCUs

  • Referenced in 9 articles [sw00128]
  • strives to avoid explosion in the resulting BDD sizes. If clustering results in a single...