FAQ 0001
Q: Can I use nuXmv in a commercial setting?
A: You may study, copy, compile and execute nuXmv only for academic,
non-commercial reaserch purposes, subject to the restrictions reported in the LICENSE.txt
You may not:

  • Modify nuXmv for any purpose.
  • Re-distribute nuXmv in any form for any purposes.
    • Examples of purposes would be running business operations, licensing, leasing,
      or selling the Software, distributing the Software for use with commercial or
      non-commercial products, using the Software in the creation or use of commercial
      or non-commercial products.

Further details are available in the License page.

FAQ 0002
Q: How can I report a bug about nuXmv?
A: There are two modalities:

  • Using the nuXmv Bug Tracker (preferred solution)
    • If needed use the following credentials
    login: anonymous
    passwd: <leave empty>
  • Sending an email to nuxmv@fbk.eu

The bug report shall contain:

  1. A brief description of the identified problem
  2. All needed information to enable us to reproduce it
    • Input files
    • Sequence of commands
  3. Any further useful information, e.g. expected behaviour.

FAQ 0003
Q: How can I subscribe/unsubscribe to the nuXmv mailing list?
A: You can subscribe by requesting to join the nuxmv-user group.

FAQ 0004
Q: Can I save a file in SMT-LIB format?
A: The SMT-LIB format is combinational in nature (similarly to a DIMACS file in the pure-boolean case).
Thus, you can not save the content of a nuXmv input file (i.e. a transition system plus a set of properties)
in SMT-LIB. However, some of the algorithms of nuXmv allow you to save combinational problems that result
from the analysis of transition systems (e.g. the unrolling up to a given depth of a bounded model checking problem).