[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 . 4 . 2 (Apr 6, 2007) We are happy to announce the availability of a new version of the NuSMV model checker. NuSMV version 2.4.2 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). 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. ======== 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 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. ---------------------------------------------------------------------- * New features ---------------------------------------------------------------------- o Improvements - Specifications using words are bit-blasted using the circuits corresponding to the functions occurring in the specification when SAT based BMC is selected for verification. This enabled the verification of models out of the scope of previous versions of NuSMV. - SAT based BMC encoding now features RBC inlining [ABE04] to reduce problem size. With RBC inlining enabled, our experiments showed on average a reduction of total model checking time. RBC inlining has also been extended to symbolic SEXP encoding to possibly benefit from its use in BDD based searches. This inlining is not enabled by default since it does not provide significant improvements on average, and in some cases it results in degraded performance. We remark that inlining might result in a dramatic degrade of performances in some cases, depending on the nature and structure of the problem. [ABE04] P. A. Abdulla, P. Bjesse and N. Eén: Symbolic Reachability Analysis Based on SAT-Solvers. In Proceedings of Tools and Algorithms for Construction and Analysis of Systems, 6th International Conference, TACAS 2000. Pages 411-425. Lecture Notes in Computer Science 1785. Springer. - SAT based BMC uses an extended version of the efficient RBC to CNF conversion described in [She04]. The new CNF conversion leads to smaller CNF than previous one, and to an average improvement in verification. Thanks to Daniel Sheridan for the preliminary version of the CNF conversion, and to Gavin Keighren for the preliminary porting to the new version of NuSMV. [She04] D. Sheridan. The Optimality of a Fast CNF conversion and its use with SAT. In Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing (SAT'2004), 10-13 May 2004, Vancouver, BC, Canada. - A patched version of CUDD-2.4.1 is now linked to NuSMV. Previous version was a patched version of CUDD-2.3.0. - Minisat2-061208 is now linked to NuSMV. Previous version was Minisat-1.14. By default NuSMV now uses the MiniSAT extended solver with simplification capabilities enabled. - New version of Zchaff-2007.3.12 can now be optionally linked to NuSMV. Previous version was zchaff-2003.12.04. - NuSMV has been ported to 64-bit architectures. It can run and compile smoothly on Intel Xeon(TM), AMD Opteron(TM), and Intel IA64(TM) architectures. We would like to thank Moshe Vardi, Kim Andrews, Franco M. Bladilo, and Jan E. Odegard from Rice University for providing us with cray facilities for testing the porting. The Cray computing facility at Rice substantially contributed to the completion of the 64-bit porting of NuSMV. o User interaction - Variable 'sexp_inlining' is used to enable/disable inlining at sexp level. Sexp inlining at the moment is applied only when BMC is performed. By default Sexp inlining is disabled. - Option -sin on|off to control new system variable sexp_inlining. - Variable 'rbc_inlining' is used to enable/disable RBC inlining before committing a problem to any SAT solver. By default RBC inlining is enabled. - Option -rin on|off to control new system variable rbc_inlining. ---------------------------------------------------------------------- * Bug fixes: ---------------------------------------------------------------------- - Fixed a bug that led to cyclic assignments not being correctly detected. Thanks to Michael Whalen and Li Zhong for reporting the bug. - Fixed a critical bug that made the booleanizer cache not take into account the contexts of booleanized formulae. Thanks to Jori Dubrovin , Tommi Junttila and Vesa Ojala for reporting the bug. - Fixed a bug that made ltl2smv fail when expanding DEFINEs containing input variables. - Fixed a bug in Incremental SBMC that resulted in false counterexamples in some cases if the property involved input variables. Thanks to Tommi Junttila for reporting the bug and also for providing a fix. - Fixed associativity of some PSL operators that were not consistent with the PSL LRM and with the core NuSMV grammar. Thanks to Andrea Fedeli for notifying us of the problem. - Applied bug fixes and cleanups suggested by Felix Rauch Valenti . Valenti and others are working on a research project in the area of static analysis, i.e. finding problems (bugs) in C/C++ source code automatically. The research project is called "Goanna" and uses NuSMV as backend. See - Fixed trace plugins that were not correctly working when words variables were used. Thanks to Vincent Gourcuff for reporting the bug. - Fixed a typo in configure.ac. Thanks to Mark Tuttle for reporting the bug. - Many other bug fixes (see Change Log) ========= 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/