
MCK
 Referenced in 33 articles
[sw09465]
 model checking as well as explicit state model checking...

JavaFAN
 Referenced in 32 articles
[sw01934]
 verify finite state programs by explicit state model checking. Both Java language and JVM bytecode...

Bebop
 Referenced in 73 articles
[sw08928]
 boolean programs. Bebop represents control flow explicitly, and sets of states implicitly using BDDs ... variable scoping, Bebop is able to model check boolean programs with several thousand lines...

SMART_
 Referenced in 33 articles
[sw04097]
 explicit and symbolic statespace generation techniques, as well as symbolic CTL modelchecking algorithms...

JNuke
 Referenced in 3 articles
[sw28382]
 combination of runtime verification, explicitstate model checking, and counterexample exploration. Efficiency...

brms
 Referenced in 31 articles
[sw19099]
 explicitly encourage users to apply prior distributions that actually reflect their beliefs. In addition, model ... assessed and compared with posterior predictive checks and leaveoneout crossvalidation...

CAESAR_SOLVE
 Referenced in 14 articles
[sw10194]
 model checking. These problems can be solved on the fly (i.e., without constructing explicitly ... equivalence checking modulo five widely used equivalence relations, onthefly model checking of regular...

ExplicitPRISMSymm
 Referenced in 2 articles
[sw13369]
 symmetry reduction technique for explicit models in PRISM. Probabilistic model checking of concurrent system involves ... property checking. In this work, we rather focus on explicitly represented probabilistic models ... report that explicitly represented models perform well at property checking, but face hurdles in model ... symmetry reduction technique for explicitly represented models. It significantly reduces build time and thus explicit...

Charlie
 Referenced in 4 articles
[sw12881]
 Petri nets, complemented by explicit CTL and LTL model checking. Charlie comes with a plugin...

Antichains
 Referenced in 33 articles
[sw20208]
 propose and evaluate a new algorithm for checking the universality of nondeterministic finite automata ... algorithm, which uses the subset construction to explicitly determinize the automaton, we keep the determinization ... algorithm experimentally using the random automaton model recently proposed by Tabakov and Vardi. We show...

CAESAR
 Referenced in 9 articles
[sw29138]
 explicitstate and onthefly verification on the generated graph, including model checking, equivalence...

DPF
 Referenced in 3 articles
[sw12853]
 Model checking database applications. We describe the design of DPF, an explicitstate model checker...

Wolf
 Referenced in 2 articles
[sw01299]
 experiments, these methods complement explicit exploration methods of software model checking...

KRATOS
 Referenced in 8 articles
[sw07808]
 programs, Kratos is capable of model checking the resulting C programs using the symbolic lazy ... novel algorithm, called ESST, that combines Explicit state techniques to deal with the SystemC Scheduler...

ODRPACK
 Referenced in 21 articles
[sw00649]
 statistics. ODRPACK can handle both explicit and implicit models, and will easily accommodate complex ... finite difference derivatives, and contains extensive error checking and report generating facilities...

SymDIVINE
 Referenced in 3 articles
[sw26690]
 SymDIVINE: a tool for bitprecise model checking of parallel C and C++ programs ... input formalism. Internally, SymDIVINE extends the standard explicitstate state space exploration with SMT machinery ... between a symbolic executor and an explicitstate model checker. The key differentiating aspect present...

TexMo
 Referenced in 1 article
[sw06913]
 which uses an explicit relation model and implements visualization, static checking, navigation, and refactoring...

Timed Rebeca
 Referenced in 3 articles
[sw40758]
 with no explicit receive. Both computation time and network delays can be modeled in Timed ... paper, we propose a new approach for checking schedulability and deadlock freedom of Timed Rebeca...

Merlin
 Referenced in 5 articles
[sw23076]
 while using tools that check for security violations caused by explicit information flow. Beginning with ... automatically infer an information flow specification. Merlin models information flow paths in the propagation graph...

dsm
 Referenced in 1 article
[sw16304]
 based approach is used to calculate spatiallyexplicit estimates of animal abundance from distance sampling ... Several utility functions are provided for model checking, plotting and variance estimation...