Version 2.6.0
Oct 14, 2015

We are happy to announce the availability of a new version of the NuSMV model checker. NuSMV version 2.6.0 is available from https://nusmv.fbk.eu.

NuSMV 2 extends the previous versions of NuSMV with several new features, most notably with the possibility of performing SAT-based Bounded Model Checking (see the Overview below).

This is a major release that comes after four years passed working under the surface. The release provides some new features, many bug fixes and optimizations, and substantial differences in the software architecture and building system.

The main changes are:

  • Splitting source code in two main components: the Core NuSMV library and the NuSMV Shell. This split enables for a much easier integration with other tools, and for a possible reorganization of the shell in the future. This change breaks backward compatibility of APIs and source code integration.
  • Switch to cmake (http://cmake.org) for building source code. This allows for a much faster build wrt previously used GNU Autotools, higher portability, and lower maintenance costs.

The bug fixes and new features are described below.

Please consider switching to nuXmv (https://nuxmv.fbk.eu). nuXmv extends NuSMV along two directions. For the verification of finite-state synchronous designs, nuXmv features strong engines based on state-of-the-art SAT-based algorithms (see the final results at the Hardware Model Checking Competition 2015 at http://fmv.jku.at/hwmcc15/). For the verification of infinite-state synchronous designs, nuXmv features state-of-the-art SMT-based verification techniques, implemented through a tight integration with the MathSAT5 SMT solver (https://mathsat.fbk.eu). For details about license terms see nuXmv's web pages.

New features

  • Language
    • NuSMV language was extended to support the min, max, and abs operators.
  • System commands
    • Added four new commands check_pslspec_bmc, check_pslspec_bmc_inc, check_pslspec_sbmc, check_pslspec_sbmc_inc. They handle the options -b (use bmc), -s (use sbmc), -i (use incremental algorithms), -c and -N previously handled by the single command check_pslspec, that now is specific for bdd-based model checking.
    • Added command convert_property_to_invar which converts LTL (CTL) properties in the form G (AG) next-expr to INVARSPEC.
    • Command print_fair_transitions now provides exact information about the fair-transitions, and not about state-input pairs. The command provides support also for dumping information in DOT and CSV formats, which is useful to visually "inspect" the FSM.
  • Command line options and system variables
    • New variable boolean_conversion_uses_predicate_normalization: When set to true, performs predicate normalization of any expression before performing the booleanization. There are cases where enabling this option pays off dramatically, however it might be expensive on other cases since the normalization of the predicates may blow up the formula. Set to false by default.
    • New variable ltl2smv_single_justice: When set to true, the tableau construction builds a degeneralized (single fairness) symbolic encoding of the Buchi automaton within ltl2smv instead of the default generalized (multiple fairness) one. Added command line option -s to ltl2smv, to enable the emit of a single justice tableau.
    • New variables pp_cpp_path and pp_m4_path to allow users to explicitly set the paths on the file system of cpp and m4 preprocessors.
  • Improvements (internal)
    • Introduced infinite-width words. In previous versione, maximum width was limited to 64.
    • RBC inlining now uses a LRU cache which always improves BMC performances (up to 30% according to our experiments).
    • Many functions were rewritten to avoid recursion. This allows for a faster executions with more limited use of stack.
    • Command help no longer relies on external files for accessing the commands' documentation. This simplify the usage.

Bug fixes

There were about 270 bug fixes, most of them were minor, but some were major issues. Here is the list of the most critical bug fixed:

  • Fixes in type checker.
  • Fixed some problems related to array handling appearing in some corner case use.
  • Fixed several issues with portability, in particular to allow compilation of core libraray with msvc-2010.

Documentation

Programmer's manual is now generated with doxygen (https://www.doxygen.org). For this reason documentation of all functions has been moved to the place of declaration (i.e. to header files). Previous documentation system has been dropped.

Source Code

Top level directory has been renamed from nusmv to "NuSMV". Source code is now located in "NuSMV/code/nusmv" with "NuSMV/code" in the inclusion path to allow for explicit inclusion of header files in the form "nusmv/..." which makes explicit where each header files is imported from.

Core library and shell have been clearly split into "NuSMV/code/nusmv/{core,shell}", and it is now possible to compile the library standalone (option ENABLE_SHELL=OFF at configuration time).

Attachment

Overview

NuSMV is a re-implementation and extension of SMV, the first model checker based on BDDs. It 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, and as a test-bed for formal verification techniques.

NuSMV version 2 extends NuSMV with new model checking algorithms and techniques. It combines classical BDD-based symbolic techniques with SAT-based techniques. It also presents other new features: for instance, it allows for a more powerful manipulation of multiple models; it can generate flat models for the whole language; it allows for cone of influence reduction.

The BDD-based model checking component exploits the CUDD library developed by Fabio Somenzi at Colorado University. The SAT-based model checking component includes an RBC-based Bounded Model Checker, connected to a SAT solver to be compiled separately (instructions and building support are batteries included in NuSMV, details are underneath). The currently available SAT solvers are: + The ZCHAFF SAT library developed by the Princeton University + The MINISAT SAT library developed by Niklas Een or Niklas Sorensson.

NuSMV version 2 is distributed with an OpenSource license, namely the GNU Lesser General Public License (LGPL). The aim is to provide a publicly available state-of-the-art symbolic model checker. With the OpenSource development model, a whole community participates in the development of a software systems, with a distributed team and independent peer review. This may result in a rapid system evolution, and in increased software quality and reliability: for instance, the OpenSource model has boosted the take-up of notable software systems, such as Linux and Apache. With the NuSMV OpenSource project, we would like to reach the same goals within the model checking community, opening the development of NuSMV.

You can find further details on NuSMV 2 and on the NuSMV project in paper:

A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. "NuSMV 2: An OpenSource Tool for Symbolic Model Checking". In Proc. CAV'02, LNCS. Springer Verlag, 2002.

Copyright

NuSMV version 2 (NuSMV 2 in short) is licensed under the GNU Lesser General Public License (LGPL in short). A copy of LGPL-2.1 can be found at url <http://www.gnu.org/licenses/lgpl.txt>.

The aim of the NuSMV OpenSource project is to allow anybody interested to participate to the development of NuSMV. To this purpose, we have chosen a license that:

  1. permits to use the system in research and commercial applications, without restrictions;
  2. is "copyleft", that is, it requires that anyone who improves the system has to make the improvements freely available.

In brief, the LGPL license allows anyone to freely download, copy, use, modify, and redistribute NuSMV 2, proviso that any modification and/or extension to the library is made publicly available under the terms of LGPL.

The license also allows the usage of the NuSMV 2 as part of a larger software system without being obliged to distributing the whole software under LGPL. Also in this case, the modification to NuSMV 2 (not to the larger software) should be made available under LGPL.

Notice that zchaff is for non-commercial purposes only. NO COMMERCIAL USE OF ZCHAFF IS ALLOWED WITHOUT WRITTEN PERMISSION FROM PRINCETON UNIVERSITY. Please contact Sharad Malik (malik@ee.princeton.edu) for details.

Notice also that the CUDD library is copyright University of Colorado. The CUDD library is not covered by LGPL.

Please contact <nusmv@list.fbk.eu> if you have any doubt or comment on the license.

Partners

Different partners have participated to the initial release of NuSMV 2. Every source file in the NuSMV 2 distribution contains a header that acknowledges the developers and the copyright holders for the file. In particular:

  • CMU and ITC-IRST contributed the source code of NuSMV version 1;
  • ITC-IRST has also developed several extensions for NuSMV 2;
  • ITC-IRST and the University of Trento have developed the SAT-based Bounded Model Checking package of NuSMV 2;
  • the University of Genova has contributed SIM, a state-of-the-art SAT solver, and the RBC package used in the Bounded Model Checking algorithms.
  • FBK-irst has developed version 2.5.0 and later.

The NuSMV team has also received several contributions for different part of the system. In particular:

  • Ariel Fuxman <afuxman@cs.toronto.edu> has extended the LTL to SMV tableau translator to the past fragment of LTL
  • Rik Eshuis <eshuis@cs.utwente.nl> has contributed a strong fairness model checking algorithm for LTL specifications
  • Dan Sheridan <dan.sheridan@contact.org.uk> has contributed several extensions and enhancements to the Bounded Model Checking algorithms.

Statements of interest have also come from several other commercial and academic institutions.

Mailing Lists

Refer to this page.

Bug Reports

We have performed an extensive test activity on NuSMV2. Still, NuSMV is large software system and contains many interacting features.

If you find a bug or misbehavior, please let us know, so that we can fix it for the next releases of NuSMV.

You can send an email to <nusmv-users@list.fbk.eu> with the description of the bug. Refer to this page for more information.

NuSMV Staff <>
https://nusmv.fbk.eu/