Release Notes

  • This is a major maintenance release that comes after 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: Switch to meson (https://mesonbuild.com) for building source code …
  • 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 …
  • This is a minor release that provides many bug fixes, some internals improvement, and a few new features. The main changes are listed below. For details please refer to the ChangeLog. New features System commands Added two new commands bmc_pick_state and bmc_inc_simulate for interactive simulations using SAT; Added option -n …
  • This is a minor release that provides many bug fixes, some internals improvement, and a few new features. The main changes are listed below. For details please refer to the ChangeLog. New features System commands Command compute has been renamed check_compute. Old command compute is deprecated. Command clean_bdd_cache has been …
  • This is a minor release that provides a few new features, and several bug fixes. The main changes are listed below. For details please refer to the ChangeLog. New minor features SMV grammar Array indices in PSL expressions can now be generic expressions, like in normal SMV grammar. Previously, only …
  • This is a minor release that provides most notably a major change in the language. It features also several bug fixes (more than 30), a few new operators in the SMV language, some new command line options, a few optimizations, and some fixes in the documentation. The main changes are …
  • Version 2.5.0 is a major release which provides new features, many optimizations and bug fixes, and an extensive reorganization of the source code and API. Many changes were driven by projects which involved FBK, like: COCONUT, COrrect-by-CONstrUcTion Workbench for Design and Verification of Embedded Systems (http://www.coconut-project …
  • Version 2.4.3 is a minor release that provides several bug fixes and commands completion when interactive shell is used. NEWS New features User interaction Added commands completion functionality to the interactive shell (requires readline library to be enabled and to be available at compile time). Thanks to Tivadar …
  • Version 2.4.2 is a minor release that provides compatibility with 64-bit architectures, speed improvements, a few extensions to the user interface and many bug fixes. Latest versions of CUDD, Minisat and Zchaff are also now used. Overall this release results on average faster than previous ones.
  • Version 2.4.1 is a minor release that provides to external contributions and some extensions to the user interface. Moreover, it fixes several bugs.
  • NuSMV 2.4.0 is a major release of NuSMV to add several new features, to improve the internal capabilities, and to fix several bugs.
  • NuSMV 2.3.1 is a minor release of NuSMV to add a few new features, and to fix several bugs.
  • NuSMV 2.3.0 is a major revision aiming to enable users to specify and check properties expressed in PSL -- the Accellera (and upcoming IEEE) standard Property Specification Language.
  • NuSMV 2.2.5 is a minor release of NuSMV to above all fix one critical bug and a few minor bugs as well.
  • NuSMV 2.2.4 is a minor release of NuSMV to add a few new features, and to fix several bugs.
  • NuSMV 2.2.3 is a minor release of NuSMV 2 to call ltl2smv internally instead of invoking an external program, to improve performances, and to fix several bugs.
  • NuSMV 2.2.2 is a minor release of NuSMV 2 to provide support for incremental Sat solving, and to fix several bugs.
  • NuSMV 2.2.1 is a minor release of NuSMV 2 to fix a problem related to BDDs dynamic variable reordering and few problems related to pre-processor invocation.
  • NuSMV 2.2 is a major release of NuSMV 2. Several improvements have been done with respect to NuSMV 2.1 (see NEWS below). The most relevant are: support for labeled transition systems improved multiple FSM management improved BDD variable ordering export of traces in different formats
  • NuSMV 2.1 is a major release of NuSMV 2. Several improvements have been done with respect to NuSMV 2.0 (see NEWS below). The most relevant are: support for past temporal operators and for strong fairness in LTL possibility to use the ZCHAFF SAT solver with Bounded Model Checking …
  • Moreover, NuSMV 2 is distributed with an OpenSource license, namely the GNU Lesser General Public License (LGPL, see the COPYRIGHT below). The aim is to provide a publicly available state-of-the-art symbolic model checker, and to allow anybody interested to participate in its development. We are looking for partners and contributors …