PV4 nuXmvchecks user-specified properties of a transition system, computes

Application domain/field

Type of tool

Model checker

Expected input


Own input language (described in the user manual)

Expected output

Depends on what is asked of nuXmv. A typical use case would be model checking (i.e. checking whether a property holds). In this case, nuXmv reports per property whether it is true. If a property is not true then it will print a counterexample.


Symbolic model checker for finite- and infinite-state transition systems and temporal logics. nuXmv has commands for model checking, model simulation, computing reachable states, predicate abstraction, model transformation, and model exploration. Moreover, it also supports the conversion of the nuXmv format into AIGER 1.9.4 and VMT (extension of SMT-LIB for symbolic transition systems). Uses MathSAT 5, CUDD, MiniSat, MSATIC3.
Model checking Simulation


Related papers

Last publication date

12 July 2019

Related tools

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.