Main.HomePage History

Hide minor edits - Show changes to output - Cancel

Changed line 25 from:
Inquiries about other usages of nuXmv should be addressed to:
to:
Inquiries about nuXmv in general and about other usages of nuXmv should be addressed to:
Changed line 17 from:
See the complete list of [[(Features.Home) | features]] provided by nuXmv or
to:
See the complete list of [[(Features.Home) | features]] provided by nuXmv, or
Changed lines 17-18 from:
See the complete list of [[(Features.Home) | features]] provided by nuXmv.
to:
See the complete list of [[(Features.Home) | features]] provided by nuXmv or
have a look at the [[https://es.fbk.eu/tools/nuxmv/downloads/nuxmv-user-manual.pdf|User Manual (pdf)]]
.
Changed lines 8-23 from:
'''nuXmv''' is a new symbolic model checker for finite- and
infinite-state
synchronous transition systems.

nuXmv is the the ''eXtended'' version of ''[[http://nusmv.fbk.eu|NuSMV]]'' open source symbolic model checker.

nuXmv builds on and extends NUSMV along two main directions:

*
For ''finite-state systems'',, it complements the basic verification techniques of NuSMV
  with state-of-the-art verification algorithms
. 
* For ''infinite-state systems'', it extends the NuSMV language with new data
  types, namely Integers and Reals, and it provides advanced SMT-based model checking
  techniques.

See [[(Features.Home) | +]] for the complete
list of the features provided by nuXmv.

nuXmv integrates the [[http
://mathsat.fbk.eu|MathSAT]] SMT solver.
to:
'''nuXmv''' is a new symbolic model checker for the analysis of synchronous finite-state and
infinite-state
systems.

nuXmv extends [[http://nusmv.fbk.eu|NuSMV]] along two main directions:

* For the finite-state case, nuXmv features a strong verification engine based on state-of-the-art SAT-based algorithms.

*
For the infinite-state case, nuXmv features SMT-based verification techniques, implemented through a tight integration with [[http://mathsat.fbk.eu|MathSAT5]].

See the complete list of [[(Features.Home) | features]] provided by nuXmv.

nuXmv is currently licensed in binary form, for non-commercial or academic purposes.

The list of nuXmv users is open for registration and discussion
-> nuxmv-users@
list.fbk.eu

Inquiries about other usages of
nuXmv should be addressed to:
-> nuxmv@list.fbk.eu
Changed line 15 from:
* For ''finite-state systems'' it complements the basic verification techniques of NuSMV
to:
* For ''finite-state systems'',, it complements the basic verification techniques of NuSMV
Changed lines 4-6 from:
(:title nuXmv :)

!! The nuXmv model checker
to:
(:title The nuXmv model checker :)

(:comment !! The nuXmv model checker :)
Changed line 3 from:
(:comment (:notitle:) :)
to:
(:comment (:notitle:)
Changed lines 3-4 from:
(:notitle:)
to:
(:comment (:notitle:) :)
(:title nuXmv
:)
Changed line 29 from:
[[http://es.fbk.eu/tools/fsap|safety assessment]], and [[https://es.fbk.eu/tools/kratos|software model checking]].
to:
[[http://fsap.fbk.eu|safety assessment]], and [[https://es.fbk.eu/tools/kratos|software model checking]].
Changed line 29 from:
[[https://es.fbk.eu/tools/fsap|safety assessment]], and [[https://es.fbk.eu/tools/kratos|software model checking]].
to:
[[http://es.fbk.eu/tools/fsap|safety assessment]], and [[https://es.fbk.eu/tools/kratos|software model checking]].
Changed line 27 from:
[[https://rat.fbk.eu|requirements analysis]],
to:
[[http://rat.fbk.eu|requirements analysis]],
Changed line 32 from:
* If you would like to cite nuXmv, please use [[Main/Reference|this reference]].
to:
If you would like to cite nuXmv, please use [[Main/Reference|this reference]].
Changed line 32 from:
If you would like to cite nuXmv, please use [[Main/Reference|this reference]].
to:
* If you would like to cite nuXmv, please use [[Main/Reference|this reference]].
Changed lines 24-26 from:
nuXmv has been used in several [[(Projects.Home) | +]] as verification back-end.

Moreover, it is the basis for several
[[(Extenstions.Home) | +]] to cope with
to:
nuXmv has been applied in  several [[(Projects.Home) | +]].

nuXmv is used as a
back-end in several [[(Extenstions.Home) | other tools]] for
Added lines 20-21:
See [[(Features.Home) | +]] for the complete list of the features provided by nuXmv.
Deleted lines 23-28:

See [[(Features.Home) | +]] for the complete list of the features provided by nuXmv.

Besides extended functionalities, the nuXmv model checker has been optimized in terms
of performance to be competitive with the state of the art.

Added line 25:
Changed line 32 from:
If you would like to cite nuXmv, please use [[Main/Reference|this reference]].
to:
If you would like to cite nuXmv, please use [[Main/Reference|this reference]].
Changed lines 7-9 from:
Welcome to the home page of the '''nuXmv''' symbolic model checker for finite and
infinite-state synchronous transition systems.
nuXmv is the the ''eXtended'' version of ''[[http://nusmv.fbk.eu|NuSMV]]'' open source symbolic model checker.
to:
'''nuXmv''' is a new symbolic model checker for finite- and
infinite-state synchronous transition systems.

nuXmv
is the the ''eXtended'' version of ''[[http://nusmv.fbk.eu|NuSMV]]'' open source symbolic model checker.
Changed lines 18-19 from:
  techniques. Currently, it uses SMT techniques implemented in
 
[[http://mathsat.fbk.eu|MathSAT]].
to:
  techniques.

nuXmv integrates the
[[http://mathsat.fbk.eu|MathSAT]] SMT solver.
Changed line 5 from:
!! nuXmv
to:
!! The nuXmv model checker
Added lines 29-31:

----
If you would like to cite nuXmv, please use [[Main/Reference|this reference]].
Changed line 12 from:
* For finite state systems it complements the basic verification techniques of NuSMV
to:
* For ''finite-state systems'' it complements the basic verification techniques of NuSMV
Changed lines 14-16 from:
* For infinite state systems, it extends the NuSMV language with new data types, namely
  Integers and
Reals, and it provides advanced SMT-based model checking techniques.
  Currently, it uses SMT techniques implemented in [[http://mathsat.fbk.eu|MathSAT]].
to:
* For ''infinite-state systems'', it extends the NuSMV language with new data
 
types, namely Integers and Reals, and it provides advanced SMT-based model checking
  techniques. Currently, it uses SMT techniques implemented in 
 
[[http://mathsat.fbk.eu|MathSAT]].
Changed line 7 from:
Welcome to the home page of the nuXmv symbolic model checker for finite and
to:
Welcome to the home page of the '''nuXmv''' symbolic model checker for finite and