
Uppaal
 Referenced in 647 articles
[sw04702]
 integrated tool environment for modeling, simulation and verification of realtime systems, developed jointly ... appropriate for systems that can be modeled as a collection of nondeterministic 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 BDDbased model checking...

Uppaal2k
 Referenced in 43 articles
[sw01595]
 integrated tool environment for modeling, simulation and verification of realtime systems, developed jointly ... appropriate for systems that can be modeled as a collection of nondeterministic processes with ... verifier of Uppaal2k. A modelchecker for automatic verification of safety and bondedliveness properties...

MCMAS
 Referenced in 73 articles
[sw09463]
 MCMAS: A Model Checker for the Verification of MultiAgent 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...

LTSAWS
 Referenced in 13 articles
[sw10585]
 LTSAWS: a tool for modelbased verification of web service compositions and choreography ... paper we describe a tool for a modelbased 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...

PRISMgames
 Referenced in 19 articles
[sw12934]
 stochastic multiplayer games, which supports modelling, automated verification and strategy synthesis for probabilistic systems...

MCMASSLK
 Referenced in 19 articles
[sw24778]
 MCMASSLK: 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 finitestate 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, onthefly model checking of regular alternationfree modal...

TAPAAL
 Referenced in 17 articles
[sw00947]
 platform independent tool for modelling, simulation and verification of timedarc Petri nets. TAPAAL provides ... simulator, while the verification module translates timedarc 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 ModelChecker for Verification and Refutation. This paper presents Yasm ... build another one? Traditional software modelcheckers build overapproximating abstractions of the programs they ... property of interest holds (verification). On the other hand, since modelcheckers 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]
 termlevel bounded model checking, correspondence checking, deductive verification, and predicate abstractionbased verification...