Features

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