The nuXmv symbolic model checker, has been used in several new tools.
Below we provide a list of known tools that builds on (directly or indirectly through other tools) nuXmv.

  • The Kratos Software Model Checker for sequential and (cooperative) threaded C programs.
  • The OCRA tool for the verification of logic-based contract refinement for embedded systems.
  • The XSAP, the eXtended version of FSAP.
  • The HyCOMP tool for the verification of hybrid systems.
  • The COMPASS tool for system-software co-engineering.
  • The AF3-OCRA plugin for the Autofocus platform by fortiss.
  • The RAT tool for requirements analysis.
  • The othelloplay tool for requirements analysis.
  • The NuGAT tool for temporal logic synthesis.
  • ...