List of model checking tools

This article lists model checking tools classified by some interesting properties. Some articles about: history and introduction to Model Checking. There are some books 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++	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 Tool	Plain	DVE input language, C/C++ (via LLVM bitcode), Timed automata	LTL		Yes	Yes	No	Yes	Free	C/C++	Unix, Windows
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
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	Windows, Linux

Modelling languages

• AltaRica: a language designed to model both functional and dysfunctional behaviours of critical systems.
• Cadence SMV: Cadence SMV Input Language; synchronous modeling language that has features supporting SMV's style of compositional refinement verification and abstract interpretation.
• CCS: Calculus of communicating systems; process calculus introduced by Robin Milner around 1980 and the title of a book describing the calculus.
• CCSP: A process calculus obtained from CCS by incorporating some operators of CSP. It is defined by Olderog and by van Glabbeek/Vaandrager.
• CSP: Communicating sequential processes; formal language for describing patterns of interaction in concurrent systems. FDR2 is a refinement checking tool for CSP, comparing two models for compatibility.
• DVE input language: a system is described as Network of Extended Finite State Machines communicating via shared variables and unbuffered channels. Does not contain support for buffered channels and for checking the type of message to be received without performing the receive proper.
• FC2: Machine-level ASCII representation for synchronized (hierarchical) networks of automata. Defined by the Esprit Basic Research Action CONCUR, 1992. Used as an input and exchange format by a number of verification tools, mainly in the area of process algebras.
• Fiacre: Format Intermédiaire pour les Architectures de Composants Répartis Embarqués.
• FSP: Finite State Processes.
• Java: Object-oriented programming language.
• LOTOS: Language Of Temporal Ordering Specification (ISO standard 8807); formal specification language based on temporal ordering used for protocol specification in ISO OSI standards.
• PEPA: Performance Evaluation Process Algebra; it is a stochastic process algebra designed for modelling computer and communication systems.
• Plain MC: these are simple text-file formats used in MRMC and PRISM.
• PRISM language: PRISM model description language.
• Promela: Process or Protocol Meta Language; it is a verification modeling language. The language allows for the dynamic creation of concurrent processes to model, for example, distributed systems.
• Reactive modules: a component-based modeling language for synchronous and asynchronous hardware and software systems
• REDLIB: Timed CTL.
• SAL: Symbolic Analysis Laboratory, a functional language with dependent types
• Simulink/Stateflow: an interactive design and simulation tool for event-driven systems.
• SCCS: synchronous calculus of communicating systems.
• SMV: SMV input language.
• TCCS: Timed CCS.
• TLA+: General-purpose specification language based on the Temporal Logic of Actions, originally used for distributed and concurrent systems. The language for the specifications and their properties is the same.
• Verilog: a hardware description language (HDL) used to model electronic systems.
• SystemVerilog: a hardware description and verification language (HDVL) used to model and verify digital electronic systems.
• VHDL: commonly used as a design-entry language for field-programmable gate arrays and application-specific integrated circuits in electronic design automation of digital circuits.

Properties language

• AFMC: Alternation Free Modal mu-Calculus.
• Assertions: Imperative assertion statements.
• CSL: Continuous Stochastic Logic, characterizes bisimulation of continuous-time Markov processes.
• CSRL: Continuous Stochastic Reward Logic; a logic to specify measures over CTMCs extended with a reward structure (so-called Markov reward models).
• CTL: Computation Tree Logic; a branching-time logic, meaning that its model of time is a tree-like structure in which the future is not determined; there are different paths in the future, any one of which might be an actual path that is realized.
• GCTL: Generalized Computation Tree Logic, it's both state based and action based.
• LTL: Linear temporal logic; a modal temporal logic with modalities referring to time.
• Monitor automata: ???.
• mCRL2 mu-calculus: Kozen's propositional modal mu-calculus (excluding atomic propositions), extended with: - data-depended processes - quantification over data types - multi actions - time - regular formulas.
• mu-calculus: temporal logics with a least fix-point operator μ.
• PCTL: Probabilistic CTL; an extension of CTL which allows for probabilistic quantification of described properties.
• PLTL: Probabilistic Linear Temporal Logic.
• PRCTL: Probabilistic Reward Computation Tree Logic; it extends PCTL with reward-bounded properties.
• PSL: Property specification language
• SVA: A subset of the SystemVerilog hardware description and verification language similar to PSL.

Abbreviations

Equivalences:

• SB: Strong Bisimulation
• WB: Weak Bisimulation
• BB: Branching Bisimulation
• STE: Strong Trace Equivalence
• WTE: Weak Trace Equivalence
• me: May Equivalence
• ME: Must Equivalence
• OE: Observational Equivalence
• SE: Safety Equivalence
• t*E: tau*.a Equivalence

Software license:

• FUSC: Free Under Specific Condition

External links

• Tools: a database for verification tools
• [1]: list of verification and synthesis tools (public domain repository on GitHub)