• NuSMV

  • Referenced in 230 articles [sw04131]
  • Information Technology at FBK-IRST 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 BDD-based model checking component that exploits the CUDD library developed ... Colorado University and SAT-based model checking component that includes an RBC-based Bounded Model...
  • PRISM

  • Referenced in 255 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 267 articles [sw04125]
  • temporal requirements are verified by symbolic model checking. If the verification fails, then HyTech generates...
  • Bandera

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

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

  • Referenced in 61 articles [sw04604]
  • SLMC: A tool for model checking concurrent systems against dynamical spatial logic specifications. The Spatial ... concurrency of Caires and Cardelli. Model-checking 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 75 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 domain-specific 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 64 articles [sw08928]
  • variable scoping, Bebop is able to model check boolean programs with several thousand lines...
  • MRMC

  • Referenced in 46 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 discrete-event simulation. This paper presents...
  • PIPER

  • Referenced in 28 articles [sw11478]
  • Types as models, model checking message-passing 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 32 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...
  • PAT

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

  • Referenced in 28 articles [sw12422]
  • Tool for Compositional Model-Checking of Real-Time Systems. In this paper we present ... tool (CMC) for compositional model-checking of real-time systems. CMC is based...
  • Cadence SMV

  • Referenced in 23 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...
  • Zing

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

  • Referenced in 35 articles [sw09480]
  • graph transformation systems, for instance using model checking...
  • APMC

  • Referenced in 20 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...
  • ARMC

  • Referenced in 18 articles [sw04949]
  • ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement. Software model checking with ... tool, called ARMC (for Abstraction Refinement Model Checking), which has already been used for practical...