NuSMV 2.1 is OUT!
Among the new features: - support for past temporal operators and for strong fairness in LTL.
- possibility to use the ZCHAFF propositional SAT solver with Bounded Model Checking.
- revision and improvement of the Bounded Model Checking package.
- a new user manual with a tutorial on the basic functionalities of NuSMV.
Read the announce for NuSMV 2.1.
Read the announce for NuSMV 2.
NuSMV 2 is OpenSource!
New versions of NuSMV are distributed under the LGPL v2.1 license. This is an Open Source license that allows free academic and commercial usage of NuSMV. For further information follow this link. 
Overview
NuSMV is a symbolic model checker developed as a joint project between the Formal Methods group in the Automated Reasoning System division at ITC- IRST, the Model Checking group at Carnegie Mellon University , the Mechanized Reasoning Group at University of Genova and the Mechanized Reasoning Group at University of Trento.
NuSMV is a reimplementation and extension of SMV, the first model checker based on BDDs. NuSMV has been designed to be an open architecture for model checking, which can be reliably used for the verification of industrial designs, as a core for custom verification tools, as a testbed for formal verification techniques, and applied to other research areas. NuSMV2, combines BDD-based model checking component that exploits the CUDD library developed by Fabio Somenzi at Colorado University and SAT-based model checking component that includes an RBC-based Bounded Model Checker, connected to the SIM SAT library developed by the University of Genova.
Project Members
Here is the list of people and institutions involved in the project. 
Getting NuSMV
Follow this link to retrieve a copy of NuSMV.
Or send an e-mail to nusmv@irst.itc.it.
NuSMV mailing lists
We maintain some mailing lists of people interested and using NuSMV.If you want to subscribe to one of the NuSMV mailing lists and be informed by e-mail on latest news about NuSMV, please:
- follow this link, or
- send an e-mail to nusmv@irst.itc.it with your name, affiliation, e-mail address and the mailing lists you want to subscribe to.
On-line documentation
NuSMV Papers
Here is the collection of papers related to NuSMV. 
NuSMV Examples
Here is the collection of NuSMV examples included in the distribution package. 
Bugs and extensions
Please help us to improve and extend NuSMV: - Report a bug.
- Submit a new example to be distributed in future releases.
- Submit new code to be distributed in future releases.
- Submit a paper about NuSMV, to be added to the NuSMV papers web page.
E-mail us