Tools using nuXmv

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 Electrum model checker for relational first-order temporal specifications
• 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.
• ...