Editing Model checking (section)

== Tools ==
{{main|List of model checking tools}}

Here is a list of significant model-checking tools:
* Afra: a model checker for [[Rebeca (programming language)|Rebeca]] which is an actor-based language for modeling concurrent and reactive systems
* [[Alloy (specification language)|Alloy]] (Alloy Analyzer)
* [[BLAST model checker|BLAST]] (Berkeley Lazy Abstraction Software Verification Tool)
* [[CADP]] (Construction and Analysis of Distributed Processes) a toolbox for the design of communication protocols and distributed systems
* [[CPAchecker]]: an open-source software model checker for C programs, based on the CPA framework
* [[ECLAIR]]: a platform for the automatic analysis, verification, testing, and transformation of C and C++ programs
* [[FDR2]]: a model checker for verifying real-time systems modelled and specified as [[Communicating sequential processes|CSP]] Processes
* [[FizzBee]]: an easier to use alternative to TLA+, that uses Python-like specification language, that has both behavioral modeling like TLA+ and probabilistic modeling like PRISM
* [[ISP Formal Verification Tool|ISP]] code level verifier for [[Message Passing Interface|MPI]] programs
* [[Java Pathfinder]]: an open-source model checker for Java programs
* [[Libdmc]]: a framework for distributed model checking
* [[mCRL2]] Toolset, [[Boost Software License]], Based on [[Algebra of Communicating Processes|ACP]]
* [[NuSMV]]: a new symbolic model checker
* [[PAT (model checker)|PAT]]: an enhanced simulator, model checker and refinement checker for concurrent and real-time systems
* [[PRISM (model checker)|Prism]]: a probabilistic symbolic model checker
* [[Romeo Model Checker|Roméo]]: an integrated tool environment for modelling, simulation, and verification of real-time systems modelled as parametric, time, and stopwatch Petri nets
* [[SPIN model checker|SPIN]]: a general tool for verifying the correctness of distributed software models in a rigorous and mostly automated fashion
* [[STORM (model checker)|Storm]]:<ref>[https://www.stormchecker.org/ Storm model checker]</ref> A model checker for probabilistic systems.
* [[TAPAs model checker|TAPAs]]: a tool for the analysis of process algebra
* [[TAPAAL]]: an integrated tool environment for modelling, validation, and verification of Timed-Arc [[Petri Nets]]
* [[TLA+]] model checker by [[Leslie Lamport]]
* [[UPPAAL]]: an integrated tool environment for modelling, validation, and verification of real-time systems modelled as networks of timed automata
* [[Zing (model-checker)|Zing]]<ref>[https://www.microsoft.com/en-us/research/project/zing Zing]</ref> – experimental tool from [[Microsoft]] to validate state models of software at various levels: high-level protocol descriptions, work-flow specifications, web services, device drivers, and protocols in the core of the operating system. Zing is currently being used for developing drivers for Windows.