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

Application domain/field

• Symbolic model checking
• Synchronous transition systems
• Finite-state systems
• Infinite-state systems

Type of tool

Model checker

Expected input

• Transition system (finite transition system (FSM) or timed transition system (TTS))
• Optional: Specification/property to check

Format:

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.

Internals

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.