This article lists model checking tools and gives an overview of the functionality of each.
The following table includes model checkers that have
In the below table, the following abbreviations are used:
Name | Model Checking | Equivalence checking | GUI | Availability | |||||||
---|---|---|---|---|---|---|---|---|---|---|---|
Plain, Probabilistic, Stochastic, ... | Modelling language | Properties language | Supported equivalences | Counter example generation | GUI | Graphical Specification | Counter example visualization | Software license | Programming language used | Platform, OS | |
BLAST | Code analysis | C | Monitor automata | Yes | No | No | No | Free | OCaml | Windows, Unix related | |
CADP | Plain and probabilistic | LOTOS, FC2, FSP, LNT | AFMC, MCL, XTL | SB, WB, BB, OE, STE, WTE, SE, tau*E | Yes | Yes | No | Yes | FUSC | C, Bourne shell, Tcl/Tk, LOTOS, LNT | macOS, Linux, Solaris, Windows |
CPAchecker | Code analysis | C | Monitor automata | Yes | Yes | No | Yes | Free | Java | Any | |
DREAM | Real-time | C++, Timed automata | Monitor automata | Yes | No | No | No | Free | C++ | Windows, Unix related | |
Java Pathfinder | Plain and timed | Java | unknown | No | Yes | No | No | Open Source Agreement | Java | macOS, Windows, Linux | |
Murφ (Murphi) | Plain | Murφ | Invariants, assertions | Yes | No | No | No | Free | C++ | Linux | |
NuSMV | Plain | SMV input language | CTL, LTL, PSL | Yes | No | No | No | Free | C | Unix, Windows, macOS | |
PAT | Plain, real-time, probabilistic | CSP#, timed CSP, probabilistic CSP | LTL, assertions | Yes | Yes | Yes | Yes | Free | C# | Windows, others with Mono | |
PRISM | Probabilistic | PEPA, PRISM language, Plain MC | CSL, PLTL, PCTL | No | Yes | No | No | Free | C++, Java | Windows, Linux, macOS | |
SPIN | Plain | Promela | LTL | Yes | Yes | No | Yes | FUSC | C, C++ | Windows, Unix related | |
TAPAAL | Real-time | Timed-Arc Petri Nets, age invariants, inhibitor arcs, transport arcs | TCTL subset | No | Yes | Yes | Yes | Free | C++, Java | macOS, Windows, Linux | |
TAPAs | Plain | CCSP | CTL, μ-calculus | SB, WB, BB, STE, WTE, me, ME, OE | Yes | Yes | Yes | Yes | Free | Java | Windows, macOS, Unix related |
UPPAAL | Real-time | Timed automata, C subset | TCTL subset | Yes | Yes | Yes | Yes | FUSC | C++, Java | macOS, Windows, Linux | |
ROMEO | Real-time | Time Petri Nets, stopwatch parametric Petri nets | TCTL subset | Yes | Yes | Yes | No | Free | C++, Tcl/Tk | macOS, Windows, Linux | |
TLA+ Model Checker (TLC) | Plain | TLA+, PlusCal | TLA | Yes | Yes | Yes | No | Free | Java | macOS, Windows, Linux |
There exists a few papers that systematically compare various model checkers on a common case study. The comparison usually discusses the modelling tradeoffs faced when using the input languages of each model checker, as well as the comparison of performances of the tools when verifying correctness properties. One can mention: