[We apologize if you received multiple copies of this message] N N SSSSS M M V V 2222 NN N S MM MM V V 2 2 N N N S M M M M V V 2 N N N u u SSSSS M M M V V 2 N N N u u S M M V V 2 N NN u u S M M V V 2 N N uuuu SSSSS M M V 222222 V E R S I O N 2 . 2 . 0 (June 10, 2004) We are happy to announce the availability of a new version of the NuSMV model checker. NuSMV version 2.2.0 is available from http://nusmv.irst.itc.it 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). 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 ======== OVERVIEW ======== NuSMV is a reimplementation 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 testbed for formal verification techniques. NuSMV version 2 extends NuSMV with new model checking algorithms and techniques. It combines classical BDD-based 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 the SIM SAT library developed by the University of Genova. Optionally, NuSMV can also be used with the ZCHAFF SAT library developed by Princeton University. 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. Further details on NuSMV 2 and on the NuSMV project can be found 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. ==== NEWS ==== This is a major release of NuSMV. Several improvements have been made with respect to NuSMV 2.1. The most relevant are: * Major changes - Input variables are now interpreted as labels over transitions in the Kripke structure. This solves several problems, including incorrect behaviors with processes. - Improved multiple FSM management, with APIs to enable composition. Improved management of encodings from scalar variables to the boolean space, with API to enable merging of encodings and other functionalities. - Packages and sub-packages have been introduced to represent the most significant data structures. Each package comes with a library, that can be linked separately from the rest of the system. New packages include different representations of FSM (i.e. Sexp, BDD, RBC), and Encodings. - Traces can be exported in different formats: textual (original), TAB separated list (to simplify import in spreadsheets), XML (for web browsing). Traces in XML format can also be imported and validated. - Improved BDD variable ordering. The reordering process can now work at the level of the boolean variables used to encode scalar variables, and the ordering file can directly refer to boolean variables. This may result in more compact BDDs (e.g. for formulae like x = y). Thanks to Dan Sheridan for the contribution. * User Interaction - Input files can now be preprocessed with multiple preprocessors (e.g. cpp, m4); the invocation order can be defined by the user. Thanks to Roger Villemaire for the interface with m4. - Trans type "Conjunctive" has been replaced by "Threshold" and is no longer supported. - Improved interactive simulator. In the choice of next states, duplicated entries are no longer present, and a distinction between state variables and input variables is enforced. Thanks to Anthony Wilder for the contribution. - Added some command line options: "-dcx", to disable counter-example generation for false properties; "-pre", to specify a list of pre-processors to be applied to the input file. * Bounded Model Checking - Improved the RBC package by introducing some new simplifications. Improved the algorithm for the generation of the CNF. Thanks to T. Junttila for the contribution. * Porting and Other - Porting under Mac OS X (see section 3 - Mac OS X in the file README_PLATFORMS for details). - Native compilation under windows using MinGW (http://www.mingw.org/). This eliminates the requirement for cygwin (http://www.cygwin.com) (see section 4 - Microsoft Windows in the file README_PLATFORMS for details). - Integration with the new version of zchaff 2003.12.04 (http://www.ee.princeton.edu/~chaff/zchaff.php); - Removed dependency on the tokens generated by yacc. * Documentation - The user manual of version 2.1 has been split in two parts: a user manual and a tutorial. - The user manual has been updated to describe new commands and functionalities. * New restrictions - Input variables can occur in LTL formulae and in fairness conditions. However, they are no longer allowed within CTL and invariant properties. - The body of DEFINEd symbols can no longer refer to next value of any variable. * Bug fixes - Fixed problems related to wrong results in presence of processes. - Fixed problems in the check for recursive definitions. - Removed BDD memory leaks in the code for dealing with LTL under full fairness. * Performance - The regression test w.r.t. version 2.1.2 pointed out an improvement in the performances of the model checking algorithms (BDD and SAT) in the majority of the considered cases. * Known bugs/problems - Some temporal formulae containing a "liberal" interpretation of truth values (e.g. "(AX p) = (AX q)") are correctly parsed, but may cause an internal error. A restriction will be enforced in the next releases. - In some cases, a significant degradation in performance of the SIM sat solver was noticed as a consequence of the new RBC package and the CNFization algorithm. The precise cause of the degradation is being investigated (notice that zchaff benefits from the changes). - Pressing Ctrl-C under Microsoft Windows Operating Systems within the interactive shell will cause unpredicatable behaviour. ========= 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 . 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 AT 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 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. The NuSMV team has also received several contributions for different part of the system. In particular: * Ariel Fuxman has extended the LTL to SMV tableau translator to the past fragment of LTL * Rik Eshuis has contributed a strong fairness model checking algorithm for LTL specifications * Dan Sheridan 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. ================ GETTING IN TOUCH ================ The home page of the NuSMV project is . For questions, comments, or information on NuSMV, please e-mail to . For getting in touch with the NuSMV development staff, please email to . ============= MAILING LISTS ============= We maintain two mailing lists on NuSMV: * nusmv-users General questions, bugs and bug fixes, possible extensions and user requests on NuSMV can be discussed on this list. * nusmv-announce New releases and other important events for NuSMV will be announced on this list. If you are interested in the usage and in the development of NuSMV, we encourage you to subscribe to these mailing lists, using the form available at url . =========== 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 use the bug report form available at url , or send an email to with the description of the bug. -- NuSMV Staff http://nusmv.irst.itc.it/