NuSMV: a new symbolic model checker
NuSMV is a symbolic model checker developed as a joint project between:
- The Embedded Systems Unit in the Digital Industry Center 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 SMV1, 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.
Latest News
nuXmv 1.0.0, a new symbolic model checker for the analysis of synchronous finite-state and infinite-state systems is OUT!
Release Notes
Version 2.6.0 Oct 14, 2015
Version 2.5.4 Oct 28, 2011
Version 2.5.3 Jun 16, 2011