The nuXmv model checker

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.