• 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 state-space generation techniques, as well as symbolic CTL model-checking algorithms...
  • JNuke

  • Referenced in 3 articles [sw28382]
  • combination of run-time verification, explicit-state model checking, and counter-example 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 leave-one-out cross-validation...
  • 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, on-the-fly 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]
  • explicit-state and on-the-fly 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 explicit-state 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 bit-precise model checking of parallel C and C++ programs ... input formalism. Internally, SymDIVINE extends the standard explicit-state state space exploration with SMT machinery ... between a symbolic executor and an explicit-state 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 spatially-explicit estimates of animal abundance from distance sampling ... Several utility functions are provided for model checking, plotting and variance estimation...