Tools

NuSMV – Symbolic Model Checker

NuSMV is a symbolic model checker developed as a joint project between: Embedded Systems Unit in...

nuXmv

nuXmv is a new symbolic model checker for finite- and infinite-state synchronous transition...

OCRA – Othello Contracts Refinement Analysis

OCRA is a tool for the verification of logic-based contracts refinement for embedded systems. It...

xSAP – The safety analysis platform

xSAP is a tool for safety assessment of synchronous finite-state and infinite-state systems....

MathSAT – Modulo Theories Solver

MathSAT 5 is an efficient Satisfiability modulo theories (SMT) solver. MathSAT 5 is the...

NuRV is an nuXmv extension for Runtime Verification (RV). NuRV supports online/offline Runtime Verification of Linear Temporal Logic (LTL) properties under assumptions given by finite- or infinite-state SMV models. NuRV can also...

FSAP – The Formal Safety Analysis Platform

FSAP aims at supporting design and safety engineers in the development and in the safety assessment of complex systems. The FSAP platform is composed of two main tools: FSAP (Formal Safety Analysis Platform), providing a graphical user interface for easier user interaction, and NuSMV-SA, an extension of the NuSMV model checker.

MBP: Model Based Planner

The Model Based Planner (MBP) is a system designed to perform plan synthesis, plan validation and...

TASTE

TASTE (The Assert Set of Tools for Engineering) is a tool-chain targeting heterogeneous embedded...

CHESS

CHESS (Composition with Guarantees for High-integrity Embedded Software Components Assembly)...

Kratos

Kratos is a software model checker for sequential and (cooperative) threaded C programs. Kratos...

Verilog2SMV

Verilog2SMV is an open source tool that takes a Verilog design with simple SystemVerilog assertions and generates a model checking problem at Register Transfer Level in SMV format. For further information, please refer...