nuXmv is a new symbolic model checker for the analysis of synchronous finite-state and infinite-state systems.
nuXmv extends 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 MathSAT5.
See the complete list of features provided by nuXmv, or have a look at the User Manual (pdf).
nuXmv is currently licensed in binary form, for non-commercial or academic purposes.
The list of nuXmv users is open for registration and discussion
Inquiries about nuXmv in general and about other usages of nuXmv should be addressed to:
nuXmv has been applied in several Related Projects.
nuXmv is used as a back-end in several other tools for requirements analysis, contract based design, model checking of hybrid systems, safety assessment, and software model checking.
If you would like to cite nuXmv, please use this reference.
