Why not getting nuXmv

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.

Getting NuSMV

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 . Before 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.

NuSMV Home page

NuSMV <>