Useful links
Model Checking Tools
NuSMV
: a reimplementation of the original CUM SMV symbolic model checker.
SPIN
: a well known explicit model checker for verifying concurrent systems including communication protocols and multithreaded programs.
Uppaal
: a model checker for verifying real-time systems.
SpaceEx
: a model checker for verifying cyber-physical systems modeled in linear hybrid automata.
IC3
: a recent breakthrough in the core model checking algorithms based on incremental inductive reasoning.
Murphi
: targeted for cache coherence protocol verification.
Building Blocks for Formal Verification Tools
MiniSAT
: a small but efficient Boolean SAT sovler. Also available at
https://github.com/niklasso/minisat
.
Yices2
: a SMT solver from SRI.
Z3
: another SMT solver from Microsoft Research.
CUDD
: A BDD package from Fabio Somenzi.
JTLV
: A Java-based environment for users to develop model checking algorithms using high-level APIs to the raw BDDs.
Uppaal DBM Library
: A C++ library for manipulating DBMs which are used to represent timing constraints in real-time state space search as in Uppaal.