Other Projects
The following links point to projects that integrate or use NuSMV:
| Tool | Description |
|---|---|
| Electrum | A model checker for relational first-order temporal specifications |
| T-Tool | T-Tool provides a framework for the effective use of formal methods in the early requirements phase. |
| MBP | Model Based Planner |
| FSAP | Legacy safety analysis tool based on the NuSMV2 tool. Superseded by xSAP. |
| PROSYD | This project aims at creating a reference methodology and a set of coherent PSL/Sugar-based tools for property-based system design. |
| ESACS | Enhanced Safety Assessment for Complex Systems |
| ISAAC | Improvement of Safety Activities on Aeronautical Complex Systems |
| AutoFOCUS3 | A tool for modeling and analyzing the structure and behavior of distributed, reactive, and timed computer-based systems. |
| MBEDDR | This project aims at creating a different way of developing embedded software systems. |
| TwoTowers | An open-source software tool for the functional verification, security analysis, and performance evaluation of computer, communication, and software systems. |
| Confluence Logic Design Language | Confluence is a functional programming language for synchronous reactive system design, including digital logic systems (ASIC, FPGA) and control oriented hard real-time software. |
| InFormal | |
| Rebeca (Reactive Objects Language) | An actor-based language with a formal foundation, designed in an effort to bridge the gap between formal verification approaches and real applications. |
| TSMV: TCTL Symbolic Model Checking of Simply-Timed Systems | An extension of NuSMV, aimed at dealing with timed versions of (models of) circuits, PLC controllers, protocols, etc. |
| Goanna: Reducing Software Bugs | An industrial-strength static analysis tool used in academia and industry alike to find bugs in C/C++ programs. Now part of Red Lizard Software. |
| RoVerGeNe | A tool for the Robust Verification of Gene Networks. |
| Graded-CTL NuSMV | An extension of NuSMV for Graded-CTL with multiple counterexamples computation. |
| nusmv-tools | Eclipse-based packages collecting some tools which interact with NuSMV. |
| nuseen | Eclipse-based environment for NuSMV, with the aim of helping NuSMV users. |
| CRISNER | A Qualitative Preference Reasoner. |
| FTS: Featured Transition Systems | |
| IVYworkbench | A model-based tool for the analysis of interactive systems designs. |
| PVSio-web 2.0 | PVSio-web is a web-based integrated development environment for the formal specification and interactive verification of interactive systems. |
| SMOF: Safety Monitoring Framework | SMOF is a framework to assist the specification of safety rules executed by an independent monitor to ensure safety of the whole system. |