NuSMV
2.4.3 is OUT!
Version 2.4.3 is a minor release that provides several bug fixes
and commands completion when interactive shell is used.
Read the announce for NuSMV 2.4.3.
Read the announce for NuSMV 2.4.2.
Read the announce for NuSMV 2.4.1.
Read the announce for NuSMV 2.4.0.
Read the announce for NuSMV 2.3.1.
Read the announce for NuSMV 2.3.0.
Read the announce for NuSMV 2.2.5.
Read the announce for NuSMV 2.2.4.
Read the announce for NuSMV 2.2.3.
Read the announce for NuSMV 2.2.2.
Read the announce for NuSMV 2.2.1.
Read the announce for NuSMV 2.2.
Read the announce for NuSMV 2.1.
Read the announce for NuSMV 2.
Added
links to other projects
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
.