spacer

NuSMV: a new symbolic model checker

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

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

    spacer Project Members

    Here is the list of people and institutions involved in the project.

    spacer Getting NuSMV

    Follow this link to retrieve a copy of NuSMV.

    Or send an e-mail to spacer .

    spacer 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 spacer with your name, affiliation, e-mail address and the mailing lists you want to subscribe to.

    spacer On-line documentation

    • NuSMV User Manual
    • NuSMV Tutorial
    • NuSMV Programmer Manual
    • NuSMV FAQ

    spacer NuSMV Papers

    Here is the collection of papers related to NuSMV.

    spacer NuSMV Examples

    Here is the collection of NuSMV examples included in the distribution package.

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

    spacer Other projects

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

    T-Tool dit.unitn.it/~ft/
    MBP mbp.fbk.eu/
    FSAP fsap.fbk.eu/
    PROSYD www.prosyd.org
    ESACS www.cert.fr/esacs/
    ISAAC www.cert.fr/isaac/
    AutoFOCUS3: a tool for modeling and analyzing the structure and behavior of distributed, reactive, and timed computer-based systems.
    		 af3.fortiss.org
    MBEDDR: this project aims at creating a different way of developing embedded software systems.
    		 www.mbeddr.com
    TwoTowers www.sti.uniurb.it/bernardo/twotowers/

    Confluence Logic Design Language

    		 www.confluent.org
    InFormal
    		 www.confluent.org/wiki/doku.php?id=informal:main
    Rebeca (Reactive Objects Language)
    		 www.rebeca-lang.org
    TSMV: TCTL Symbolic Model Checking of Simply-Timed Systems
    		 www.lsv.ens-cachan.fr/~markey/TSMV
    Goanna: Reducing Software Bugs
    		 www.ertos.nicta.com.au/research/goanna
    Goanna is now part of Red Lizards:
    		 www.redlizards.com
    RoVerGeNe: A tool for the Robust Verification of Gene Networks
    		 iasi.bu.edu/~batt/rovergene/rovergene.htm
    Graded-CTL NuSMV: An extension of NuSMV for Graded-CTL with multiple counterexamples computation
    		 gradedctl.dia.unisa.it
    nusmv-tools: Eclipse-based packages collecting some tools which interact with NuSMV
    		 code.google.com/a/eclipselabs.org/p/nusmv-tools/
    nuseen: Eclipse-based environment for NuSMV, with the aim of helping NuSMV users
    		 https://code.google.com/a/eclipselabs.org/p/nuseen/
    CRISNER: A Qualitative Preference Reasoner
    		 www.ece.iastate.edu/~gsanthan/crisner.html

    spacer E-mail us

    For information about NuSMV, please send e-mail to spacer . For asking support or bug reporting write instead to spacer . Please note that we will forward to the latter any technical mail sent to spacer , so to allow all our users to benefit from the answers.
    NuSMV <spacer >
    Related searches:
    announce checking checker symbolic project
    gipoco.com is neither affiliated with the authors of this page nor responsible for its contents. This is a safe-cache copy of the original web site.