NuSMV: a new symbolic model checker

NuSMV 2.5.0 is OUT!

Version 2.5.0 is a major release which provides new features, many optimizations and bug fixes, and an extensive reorganization of the source code and API.

Links to some projects using NuSMV

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

Other projects

The following links point to projects that integrate or use NuSMV:

`T-Tool`	http://dit.unitn.it/~ft/
MBP	http://sra.itc.it/tools/mbp/
FSAP	http://sra.itc.it/tools/FSAP
PROSYD	http://www.prosyd.org
ESACS	http://www.cert.fr/esacs/
ISAAC	http://www.cert.fr/isaac/
TwoTowers	http://www.sti.uniurb.it/bernardo/twotowers/
Confluence Logic Design Language	http://www.confluent.org
InFormal	http://www.confluent.org/wiki/doku.php?id=informal:main
Rebeca (Reactive Objects Language)	http://khorshid.ece.ut.ac.ir/~rebeca/index.htm
TSMV: TCTL Symbolic Model Checking of Simply-Timed Systems	http://www.lsv.ens-cachan.fr/~markey/TSMV
Goanna: Reducing Software Bugs	http://www.ertos.nicta.com.au/research/goanna
Goanna is now part of Red Lizards:	http://www.redlizards.com
RoVerGeNe: A tool for the Robust Verification of Gene Networks	http://iasi.bu.edu/~batt/rovergene/rovergene.htm
Graded-CTL NuSMV: An extension of NuSMV for Graded-CTL with multiple counterexamples computation	http://gradedctl.dia.unisa.it

E-mail us

For information about NuSMV, please send e-mail to

NuSMV <