NuSMV: a new symbolic model checker

NuSMV 2.5.4 is OUT!

NuSMV 2.5.4 is a minor release that provides many bug fixes, some internals improvement, and a few new features.

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 Embedded Systems Unit in the Center for Information Technology at FBK-IRST

The Model Checking group at Carnegie Mellon University , the Mechanized Reasoning Group at University of Genova

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, which can be connected to the Minisat SAT Solver and/or to the ZChaff SAT Solver. The University of Genova has contributed SIM, a state-of-the-art SAT solver used until version 2.5.0, and the RBC package use in the Bounded Model Checking algorithms.

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://mbp.fbk.eu/
FSAP	http://fsap.fbk.eu/
PROSYD	http://www.prosyd.org
ESACS	http://www.cert.fr/esacs/
ISAAC	http://www.cert.fr/isaac/
AutoFOCUS3: a tool for modeling and analyzing the structure and behavior of distributed, reactive, and timed computer-based systems.	http://af3.fortiss.org
MBEDDR: this project aims at creating a different way of developing embedded software systems.	http://www.mbeddr.com
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://www.rebeca-lang.org
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
nusmv-tools: Eclipse-based packages collecting some tools which interact with NuSMV	http://code.google.com/a/eclipselabs.org/p/nusmv-tools/

E-mail us

For information about NuSMV, please send e-mail to

NuSMV <