Formal Methods Tools

Model Checking Tools

This page lists all of the model checking tools on this site in alphabetical order. Click a tool name in the first column to view tool details. Click a colorful item in the second column to view all the tools for which that term applies. Item colors mean nothing and are intended to make it easy to skim the page. Colors are generated by hashing each term’s name and converting it to RGB color values.

Tool Applications Licenses
Model Checker CRAPL
ABC Theorem Prover Model Checker MIT
AVR Model Checker GPL-3.0
Model Checker Apache-2.0
CADP Model Checker All Rights Reserved
CGAAL Model Checker AGPL-v3
Concuerror Model Checker BSD-2-Clause
CPAchecker Model Checker Apache-2.0
DSCheck Model Checker ISC
Eldarica Model Checker BSL
ESBMC Model Checker Apache-2.0 BSD 4-clause MIT BSD 3-clause GPLv3
Fast Downward PDR Model Checker GPL-3.0
fbPDR Model Checker MIT
Model Checker GPL-3.0
Geyser Model Checker MIT
IMITATOR Parameter Synthesizer GPLv3
ImSpin Model Checker MIT
Model Checker BSD-3-Clause
IVy
Protocol Verifier MIT
Kind 2 Model Checker Apache-2.0
Model Checker
LTSmin Model Checker BSD-3-Clause
Model Checker
mCRL2 Model Checker BSL
Model Checker MIT
Model Checker MIT
NuSMV Model Checker LGPL
NuXMV Model Checker All Rights Reserved
PDRC Model Checker
Pnmc Model Checker BSD-2-Clause
pyPL Model Checker Model Generator Theorem Prover Unilicense
Reach Model Checker MIT
rIC3 Model Checker GPL-3.0
Roméo Model Checker GPL
Rumur Model Checker Unilicense
Sally Model Checker GPLv2
Model Checker GPL-3.0
SM(P/)T Model Checker GPLv3
SpaceEx Hybrid Systems GPLv3
Spin Model Checker All Rights Reserved
stateright Model Checker MIT
TAPAAL Model Checker GPL-2.0
Model Checker
Uppaal Model Checker All Rights Reserved
Model Checker
Red dot indicates tool has not been updated or maintained recently