NuSMV: a new symbolic model checker


nuXmv 1.0.0 a new symbolic model checker for the analysis of synchronous finite-state and infinite-state systems is OUT

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.
Follow this link to retrieve a copy.

Read the announce for NuSMV 2.5.4.
Read the announce for NuSMV 2.5.3.
Read the announce for NuSMV 2.5.2.
Read the announce for NuSMV 2.5.1.
Read the announce for NuSMV 2.5.0.
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.

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:

    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 . For asking support or bug reporting write instead to . Please note that we will forward to the latter any technical mail sent to , so to allow all our users to benefit from the answers.

    NuSMV < >