
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 BDDbased model checking component that exploits...

Esterel
 Referenced in 163 articles
[sw20012]
 also provide support for explicit or BDDbased verification tools that perform either bisimulation reduction...

MONA
 Referenced in 122 articles
[sw06170]
 tree automata, threevalued logic, eager minimization, BDDbased automata representations, and cacheconscious data...

Rabbit
 Referenced in 24 articles
[sw01317]
 Rabbit: A tool for BDDbased verification of realtime 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 BDDbased 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 BDDbased model checking algorithms...

azove
 Referenced in 12 articles
[sw04634]
 outputsensitive$ algorithm for building a BDD for a linear constraint (a socalled 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 (BDDbased) reachability, distributed reachability (MPIbased...

MCMASSLK
 Referenced in 17 articles
[sw24778]
 logic specifications. We introduce MCMASSLK, a BDDbased 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 BDDrepresented 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 worsecase...

SBSAT
 Referenced in 10 articles
[sw00828]
 SBSAT: a statebased, BDDbased 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 multiterminal BDD based representation of automata and has implemented algorithms...

TRANSYT
 Referenced in 7 articles
[sw00976]
 TRANSYT is a BDDbased 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]
 worstcase bounds of the best BDDbased 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...