For a detailed description of the features provided by nuXmv, we suggest to read the User Manual (pdf).

Below we list the most important ones.

  • An extended language for synchronous systems
    • Support for the AIGER format
    • New set of types, namely 'Integer' and 'Reals', and Uninterpreted Functions
    • New dumps of model in several external formats
      • AIGER, VMT, BTOR (this last via an external script)
  • New model checking algorithms for finite-state systems
    • Interpolation based invariant checking
      • CAV'03 Mc Millan's interpolation algorithm
      • Interpolation sequences algorithm
    • IC3 based algorithms
    • K-liveness
    • Guided reachability
      • Reachability analysis and invariant checking guided by a regular expression
  • New model checking algorithms for infinite-state systems
    • SMT-based techniques
      • Bounded Model Checking
      • K-induction
      • K-liveness
      • Interpolation Based
      • IC3 based algorithms
    • Abstraction based techniques
      • Counter-Example Guided Abstraction Refinement (CEGAR)
        • Refinement via Unsatisfiable Core and Interpolation
      • K-induction with implicit abstraction
        • Refinement via Unsatisfiable Core and Interpolation
      • IC3 with implicit abstraction
  • An extended set of functionalities
    • Explicit FSM view generation
      • Dump in .xmi format
      • Subject to predicate abstraction
    • Model simplification and recoding techniques
      • Range Recoding
      • Free input propagation