
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, timeseries 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 symbolicstatistical modeling. We present an overview of symbolicstatistical modeling ... describe various types of symbolicstatistical 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 preimages ... 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]
 opensource fixedpoint model checker for symbolic analysis of security protocols. We introduce ... opensource fixedpoint 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, constraintbased techniques, which are correct and terminating...

Quantor
 Referenced in 22 articles
[sw28381]
 such as nondeterministic 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 modelchecking 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 inputoutput 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 socalled 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 OBDDbased symbolic model checking algorithm to efficiently determine whether specifications...