
NuSMV
 Referenced in 264 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...

PRISM
 Referenced in 336 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...

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

Bandera
 Referenced in 128 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 110 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 100 articles
[sw10692]
 abstracting PEPA models, and for model checking properties in the Continuous Stochastic Logic (CSL). Download...

MRMC
 Referenced in 65 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...

SLMC
 Referenced in 63 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...

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

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...

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

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 33 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...

CMC
 Referenced in 31 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...

PAT
 Referenced in 26 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...

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

Cadence SMV
 Referenced in 26 articles
[sw07795]
 Cadence SMV is a symbolic model checking tool that allows you to formally verify temporal ... verification is often equated with equivalence checking, model checking is substantially more general. It allows ... design process by building abstract system level models. Its use continues through the design refinement...

MCK
 Referenced in 22 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...

APMC
 Referenced in 24 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...

Zing
 Referenced in 38 articles
[sw01037]
 Zing is a software model checking project at Microsoft Research. Our goal is to build...