List of model checking tools

This article lists model checking tools classified by some interesting properties. Some articles about: history[1] and introduction[2] to Model Checking. There are some books[3] that deal with model checking techniques.

Comparison of some model checking tools

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
APMC Approximate Probabilistic Reactive modules PCTL, PLTL No Yes No No FUSC C Unix & related
ARC Plain AltaRica μ-calculus, CTL* Yes Yes No No FUSC ANSI C Unix & related
BANDERA Code analysis Java CTL, LTL Yes Yes Yes Yes Free Java Windows and Unix related
BLAST Code analysis C Monitor automata Yes No No No Free OCaml Windows and Unix related
CADENCE SMV Plain Cadence SMV, SMV, Verilog CTL, LTL Yes Yes No No FUSC ? Windows and Unix related
CADP Probabilistic LOTOS, FSP, LOTOS NT AFMC SB, WB, BB, OE, STE, WTE, SE, tau*E Yes Yes Yes Yes FUSC ? Mac OS, Linux, Solaris, Windows
CBMC Code analysis C, C++, Java Assertions Yes Yes No No Free C++ Windows and Unix related
CPAchecker Code analysis C Monitor automata Yes Yes No Yes Free Java Any
CWB-NC Plain and Timed CCS, CSP, LOTOS, TCCS AFMC, CTL, GCTL SB, WB, me, ME Yes Yes No No FUSC SML Windows and Unix related, Mac OS
DBRover Timed Ada, C, C++, Java, VHDL, Verilog LTL, MTL No Yes Yes Yes Non-free Commercial use only ? Windows and Unix related
DIVINE Plain C/C++ (via LLVM bitcode), DVE input language, Timed automata LTL, Assertions, Memory safety Yes Yes No Yes Free C/C++ Unix and related
DREAM Real-time C++, Timed automata Monitor automata Yes No No No Free C++ Windows and Unix related
DSVerifier Digital system analysis C, C++ Assertions Yes Yes No No Free C++ Windows and Unix related
EBMC Model checking SMV, Verilog SVA Yes Yes No No Free C++ Windows and Unix related
Edinburgh CWB Plain CCS, TCCS, SCCS μ-calculus SB, WB, BB, me, ME, OE Yes No No No FUSC SML Windows and Unix related
EmbeddedValidator Hybrid Simulink/Stateflow/TargetLink/C Monitor automata Yes Yes Yes Yes Non-free Commercial use only ? Windows
ESBMC Code analysis C, C++ Assertions Yes Yes No No Free C++ Windows and Unix related
Expander2 Hybrid AFMC, CTL SB, OE No Yes No No Free O'Haskell Unix related
Fc2Tools Plain FC2 ? SB, WB, BB Yes No Yes Yes Free ? Unix related
GEAR Plain ? AFMC, CTL, μ-calculus Yes Yes Yes Yes Free Java Windows and Unix related
ImProve Plain Haskell Assertions Yes No No No Free Haskell Linux, Windows, Mac-OS
Java Pathfinder Plain and timed Java unknown No Yes No No NOSA Java Mac OS, Windows, Linux
LLBMC Code analysis C, C++, all languages supported by LLVM Assertions Yes No No No FUSC C++ Windows and Unix related
LTSA Plain FSP LTL Yes Yes No Yes Free Java Windows and Unix related
LTSmin Plain, Real-time Promela, μCRL, mCRL2, DVE Input Language μ-calculus, LTL, CTL* SB, BB Yes No No No Free C, C++ Unix, Mac OS X, Windows
MCMAS Plain, Epistemic ISPL CTL, CTLK Yes Yes No Yes Free C++ Unix, Windows, Mac-OS
mCRL2 Plain, Real-time mCRL2 μ-calculus SB, BB, t*E, STE, WTE Yes Yes No Yes Free C++ Mac OS, Linux, Solaris, Windows
MRMC Real-time, Probabilistic Plain MC CSL, CSRL, PCTL, PRCTL SB No No No No Free C Windows, Linux, Mac OS
NuSMV Plain SMV CTL, LTL, PSL Yes No No No Free C Unix, Windows, Mac OS X
ompca, OpenMP C Analysis software symbolic simulation with API control C/C++ programs with OpenMP directives logic predicates or flexible procedures through API Yes Yes No Yes Free C, C++ Ubuntu Linux, Windows version available soon
PAT Plain,Real-time,Probabilistic CSP#, Timed CSP, Probabilistic CSP LTL, Assertions Yes Yes Yes Yes Free C# Windows, other OS with Mono
PRISM Probabilistic PEPA, PRISM language, Plain MC CSL, PLTL, PCTL No Yes No No Free C++, Java Windows, Linux, Mac OS
ProB Plain B-Method, Event-B, Z, TLA+, CSP Assertions, LTL, CTL Yes Yes No Yes Free Prolog, C, Java, Tcl/Tk Linux, Mac OS, Windows
Reactis Tester Hybrid Simulink/Stateflow ? No Yes Yes No Non-free Commercial use only SML Windows, Linux
RED dense-time, linear hybrid, fully symbolic communicating timed automata (CTA), linear-hybrid automata (LHA) TCTL with fairness assumptions, CTA with fairness assumptions timed simuilation, fair simulation Yes Yes Yes Yes Free C/C++ Ubuntu Linux
SAL symbolic, bounded, and infinite SAL LTL Yes No No No GPL Scheme Linux, Mac OS X, Windows (Cygwin)
SATABS Code analysis C, C++ Assertions Yes Yes No No Free C++ Windows and Unix related
SATMC Plain, bounded ASLan, ASLan++ LTL, Assertions Yes No No No Free Prolog Windows and Unix related
SLMC Plain pi-calculus CCL Yes No No No Free OCaml Windows and Unix related
SPIN Plain Promela LTL Yes Yes No Yes FUSC C, C++ Windows and Unix related
Spot Plain Petri nets, DVE Input Language LTL, PSL subset Yes No No No Free C, C++ Unix & related
TAPAAL Real-time Timed-Arc Petri Nets, age invariants, inhibitor arcs, transport arcs TCTL subset No Yes Yes Yes Free C++, Java Mac OS, Windows, Linux
TAPAs Plain CCSP CTL, μ-calculus SB, WB, BB, STE, WTE, me, ME, OE Yes Yes Yes Yes Free Java Windows, Mac OS and Unix related
UPPAAL Real-time Timed automata, C subset TCTL subset Yes Yes Yes Yes FUSC C++, Java Mac OS, Windows, Linux
ROMEO Real-time Time Petri Nets, stopwatch parametric Petri nets TCTL subset Yes Yes Yes No Free C++, tcl/tk Mac OS, Windows, Linux
TLC Plain TLA+, PlusCal TLA Yes Yes Yes No Free Java Mac OS, Windows, Linux

Modelling languages

Properties language

Abbreviations

Equivalences:

Software license:

References

External links

This article is issued from Wikipedia - version of the 9/12/2016. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.