• PRISM

  • Referenced in 442 articles [sw01186]
  • PRISM: Probabilistic symbolic model checker. In this paper we describe PRISM, a tool being developed ... tool features three model checking engines: one symbolic, using BDDs (binary decision diagrams) and MTBDDs...
  • R

  • Referenced in 9810 articles [sw00771]
  • wide variety of statistical (linear and nonlinear modelling, classical statistical tests, time-series analysis, classification ... quality plots can be produced, including mathematical symbols and formulae where needed. Great care...
  • HyTech

  • Referenced in 331 articles [sw04125]
  • temporal requirements are verified by symbolic model checking. If the verification fails, then HyTech generates...
  • NuSMV

  • Referenced in 309 articles [sw04131]
  • NuSMV is a symbolic model checker developed as a joint project between: The Embedded Systems...
  • Bebop

  • Referenced in 73 articles [sw08928]
  • Bebop: A Symbolic Model Checker for Boolean Programs. We present the design, implementation and empirical ... evaluation of Bebop—a symbolic model checker for boolean programs. Bebop represents control flow explicitly...
  • PRISM

  • Referenced in 39 articles [sw23359]
  • PRISM: A language for symbolic-statistical modeling. We present an overview of symbolic-statistical modeling ... describe various types of symbolic-statistical modeling formalism known but unrelated...
  • nuXmv

  • Referenced in 28 articles [sw18526]
  • nuXmv Symbolic Model Checker. This paper describes the nuXmv symbolic model checker for finite...
  • APMC

  • Referenced in 28 articles [sw11483]
  • Approximate probabilistic model checking. Symbolic model checking methods have been extended recently to the verification...
  • Cadence SMV

  • Referenced in 27 articles [sw07795]
  • Cadence SMV is a symbolic model checking tool that allows you to formally verify temporal...
  • Mcmt

  • Referenced in 24 articles [sw11911]
  • mcmt, a fully declarative and deductive symbolic model checker for safety properties of infinite state ... system is a backward reachability procedure which symbolically computes pre-images ... heuristics for quantifier instantiation, specifically tailored to model checking, are at the very heart...
  • SCOTS

  • Referenced in 17 articles [sw20172]
  • nonlinear control systems based on symbolic models, also known as discrete abstractions. The tool accepts ... discretization parameters to compute a symbolic model that is related with the original control system...
  • OFMC

  • Referenced in 28 articles [sw09466]
  • open-source fixed-point model checker for symbolic analysis of security protocols. We introduce ... open-source fixed-point model checker OFMC for symbolic security protocol analysis, which extends ... model checker (the previous OFMC). The native input language of OFMC is the AVISPA Intermediate ... integration of a number of symbolic, constraint-based techniques, which are correct and terminating...
  • Quantor

  • Referenced in 22 articles [sw28381]
  • such as non-deterministic planning or symbolic model checking can be formulated succinctly...
  • SMART_

  • Referenced in 33 articles [sw04097]
  • same modeling study. For the analysis of logical behavior, both explicit and symbolic state ... space generation techniques, as well as symbolic CTL model-checking algorithms, are available...
  • Sigma*

  • Referenced in 11 articles [sw21731]
  • Sigma*, a novel technique for learning symbolic models of software behavior. Sigma* addresses the challenge ... synthesizing models of software by using symbolic conjectures and abstraction. By combining dynamic symbolic execution ... discover symbolic input-output steps of the programs and counterexample guided abstraction refinement to over ... relative to abstraction. To represent inferred symbolic models, we use a variant of symbolic transducers...
  • SHARPE

  • Referenced in 43 articles [sw03100]
  • SHARPE, (Symbolic Hierarchical Automated Reliability and Performance Evaluator) is a tool for specifying and analyzing ... performance, reliability and performability models. It has been installed at over 250 sites...
  • Akiss

  • Referenced in 15 articles [sw20605]
  • works in the so-called symbolic model, representing protocols by processes in the applied...
  • MBSymba

  • Referenced in 12 articles [sw04274]
  • Then, a set of methods for symbolic modeling of multibody systems is explained. The first ... formulation, reobtaining the well known Sharp’s model of the straight running of the motorcycle ... power of the given symbolic procedures and shows how a model suitable for stability, handling...
  • SMV

  • Referenced in 13 articles [sw04135]
  • syntax. SMV uses the OBDD-based symbolic model checking algorithm to efficiently determine whether specifications...