|nuXmv 1.0.0 a new symbolic model checker for the analysis of synchronous finite-state and infinite-state systems is OUT. You may have a try.|
| NuSMV v2 is open source software and it is
distributed under LGPL v2.1
license. For more information about the availability and the use
of NuSMV v2 please send an e-mail to
downloading NuSMV v2 please carefully read the LGPL license.|
|NuSMV v1.1 can be used, free of charge, only by academic institutions and only for their internal research and educational purposes.|
|NuSMV source|| The NuSMV source code.
|NuSMV binaries|| Pre-compiled versions of NuSMV.