• Uppaal

  • Referenced in 647 articles [sw04702]
  • integrated tool environment for modeling, simulation and verification of real-time systems, developed jointly ... appropriate for systems that can be modeled as a collection of non-deterministic processes with...
  • HyTech

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

  • Referenced in 305 articles [sw04131]
  • architecture for model checking, which can be reliably used for the verification of industrial designs ... formal verification techniques, and applied to other research areas. NuSMV2, combines BDD-based model checking...
  • Uppaal2k

  • Referenced in 43 articles [sw01595]
  • integrated tool environment for modeling, simulation and verification of real-time systems, developed jointly ... appropriate for systems that can be modeled as a collection of non-deterministic processes with ... verifier of Uppaal2k. A model-checker for automatic verification of safety and bonded-liveness properties...
  • MCMAS

  • Referenced in 73 articles [sw09463]
  • MCMAS: A Model Checker for the Verification of Multi-Agent Systems. While temporal logic...
  • Design/CPN

  • Referenced in 37 articles [sw01952]
  • Modeling and verification of cryptographic protocols using coloured Petri nets and Design/CPN...
  • UNITY

  • Referenced in 185 articles [sw13461]
  • models. The methodology starts with a simulation model specification in the form ... formal assertions, permitting formal verification of the transition systems, and second into an executable program ... specify properties formally that the model should obey and prove them as theorems using...
  • LTSA-WS

  • Referenced in 13 articles [sw10585]
  • LTSA-WS: a tool for model-based verification of web service compositions and choreography ... paper we describe a tool for a model-based approach to verifying compositions ... tool supports verification of properties created from design specifications and implementation models to confirm expected ... providing cooperating tools for specification, formal modeling, verification and validation of the composition process...
  • MOCHA

  • Referenced in 91 articles [sw12935]
  • Model Checking. MOCHA is a growing interactive software environment for system specification and verification...
  • ISP

  • Referenced in 12 articles [sw04895]
  • Order”) is a tool for the formal verification of MPI(Message Passing Interface) programs developed ... Computing at the University of Utah. Like model checkers, such as SPIN, ISP verifies ... safety properties. However, unlike model checkers, ISP performs code level verification. This means that ... actual program code without building verification models. ISP has been used to successfully verify...
  • PRISM-games

  • Referenced in 19 articles [sw12934]
  • stochastic multi-player games, which supports modelling, automated verification and strategy synthesis for probabilistic systems...
  • MCMAS-SLK

  • Referenced in 19 articles [sw24778]
  • MCMAS-SLK: A model checker for the verification of strategy logic specifications. We introduce MCMAS ... based model checker for the verification of systems against specifications expressed in a novel, epistemic...
  • GROOVE

  • Referenced in 50 articles [sw09480]
  • VErification (GROOVE). GROOVE is a project centered around the use of simple graphs for modelling...
  • STeP

  • Referenced in 36 articles [sw17948]
  • systems, but combines model checking with deductive methods to allow the verification of a broad...
  • CAESAR_SOLVE

  • Referenced in 14 articles [sw10194]
  • Bess) provide a useful framework for modeling various verification problems on finite-state concurrent systems ... such as equivalence checking and model checking. These problems can be solved ... library has been developed within the Cadp verification toolbox using the generic Open/Caesar environment ... widely used equivalence relations, on-the-fly model checking of regular alternation-free modal...
  • TAPAAL

  • Referenced in 17 articles [sw00947]
  • platform independent tool for modelling, simulation and verification of timed-arc Petri nets. TAPAAL provides ... simulator, while the verification module translates timed-arc Petri net models into networks of timed...
  • SMACK

  • Referenced in 9 articles [sw23311]
  • simplifies the implementation of algorithms for verification, model checking, and abstract interpretation...
  • YASM

  • Referenced in 12 articles [sw09470]
  • Yasm: A Software Model-Checker for Verification and Refutation. This paper presents Yasm ... build another one? Traditional software model-checkers build over-approximating abstractions of the programs they ... property of interest holds (verification). On the other hand, since model-checkers are widely known...
  • UMM

  • Referenced in 8 articles [sw10132]
  • features to support memory model verification: (i) it employs a simple and generic memory abstraction ... capture a large collection of memory models as guarded commands with a uniform notation...
  • UCLID

  • Referenced in 25 articles [sw04657]
  • term-level bounded model checking, correspondence checking, deductive verification, and predicate abstraction-based verification...