
PRISM
 Referenced in 442 articles
[sw01186]
 Markov chains. Analysis is performed through model checking such systems against specifications written ... tool features three model checking engines: one symbolic, using BDDs (binary decision diagrams) and MTBDDs...

NuSMV
 Referenced in 309 articles
[sw04131]
 Information Technology at FBKIRST The Model Checking group at Carnegie Mellon University , the Mechanized ... open architecture for model checking, which can be reliably used for the verification of industrial ... research areas. NuSMV2, combines BDDbased model checking component that exploits the CUDD library developed ... Colorado University and SATbased model checking component that includes an RBCbased Bounded Model...

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

Bandera
 Referenced in 134 articles
[sw07663]
 Using the Bandera tool set to modelcheck properties of concurrent Java software. The Bandera ... components designed to facilitate experimentation with modelchecking Java source code. Bandera takes as input ... language of one of several existing modelchecking tools (including Spin, dSpin ... model to the property being checked. When a modelchecker produces an error trail, Bandera...

Java PathFinder
 Referenced in 123 articles
[sw07658]
 Model checking JAVA programs using JAVA PathFinder. The paper describes a translator called JAVA PATHFINDER ... which translates from JAVA to PROMELA, the modeling language of the SPIN model checker ... PROMELA model, which then can be model checked using SPIN. The JAVA program may contain ... translated into similar assertions in the PROMELA model. The PSIN model checker will then look...

PEPA
 Referenced in 117 articles
[sw10692]
 abstracting PEPA models, and for model checking properties in the Continuous Stochastic Logic (CSL). Download...

SLMC
 Referenced in 74 articles
[sw04604]
 SLMC: A tool for model checking concurrent systems against dynamical spatial logic specifications. The Spatial ... concurrency of Caires and Cardelli. Modelchecking is one of the most widely used techniques ... check temporal properties of software systems. However, when the analysis focuses on properties related ... outperforms other tools for verifying systems modeled in πcalculus...

MRMC
 Referenced in 71 articles
[sw04129]
 models. It supports PCTL and CSL model checking, and their reward extensions. Distinguishing features ... Markov decision processes (CTMDPs) and CSL model checking by discreteevent simulation. This paper presents...

MOCHA
 Referenced in 92 articles
[sw12935]
 MOCHA: Modularity in Model Checking. MOCHA is a growing interactive software environment for system specification...

Bebop
 Referenced in 73 articles
[sw08928]
 variable scoping, Bebop is able to model check boolean programs with several thousand lines...

Bogor
 Referenced in 36 articles
[sw06858]
 model checker using the Bogor extensible model checking framework Model checking has proven ... developed suggest that domainspecific model checking engines may be more effective than general purpose ... model checking tools. To overcome limitations of existing tools which tend to be monolithic ... have developed an extensible and customizable model checking framework called Bogor. In this tool paper...

MCK
 Referenced in 33 articles
[sw09465]
 Model checking knowledge. MCK is a model checker for the logic of knowledge, developed ... variety of approaches to model checking the logic of knowledge. The novelty of this model ... were based primarily on BDDbased model checking algorithms, but MCK now also supports bounded ... model checking as well as explicit state model checking...

PAT
 Referenced in 36 articles
[sw13258]
 simulator. Most importantly, PAT implements various model checking techniques catering for different properties such ... fairness assumptions, refinement checking and probabilistic model checking. To achieve good performance, advanced optimization techniques ... symmetry reduction, process counter abstraction, parallel model checking...

DiVinE
 Referenced in 56 articles
[sw04130]
 DIVINE is a tool for LTL model checking and reachability analysis of discrete distributed systems...

WASP
 Referenced in 55 articles
[sw09565]
 atom support, and techniques for stable model checking. Concerning the branching heuristics, WASP adopts...

PIPER
 Referenced in 28 articles
[sw11478]
 Types as models, model checking messagepassing programs. Abstraction and composition are the fundamental issues ... making model checking viable for software. This paper proposes new techniques for automating abstraction ... proof rule for carrying out compositional model checking on the types. Open simulation between ... abstraction relation for compositional model checking. We have implemented these ideas in a tool – PIPER...

WSAT
 Referenced in 37 articles
[sw01022]
 with the state of the art model checking techniques. Web services are loosely coupled distributed ... several challenges in the application of model checking: (1) Numerous competing web service standards, most ... based manipulation are not supported by current model checkers...

GROOVE
 Referenced in 51 articles
[sw09480]
 graph transformation systems, for instance using model checking...

CMC
 Referenced in 34 articles
[sw12422]
 Tool for Compositional ModelChecking of RealTime Systems. In this paper we present ... tool (CMC) for compositional modelchecking of realtime systems. CMC is based...

APMC
 Referenced in 28 articles
[sw11483]
 Approximate probabilistic model checking. Symbolic model checking methods have been extended recently to the verification ... induce a prohibitive cost for the model checking algorithm. In this paper, we propose...