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...
Read MoreTools
xSAP – The safety analysis platform
xSAP is a tool for safety assessment of synchronous finite-state and infinite-state systems....
Read More
NuSMV – Symbolic Model Checker
NuSMV is a symbolic model checker developed as a joint project between: Embedded Systems Unit in...
Read More
OCRA – Othello Contracts Refinement Analysis
OCRA is a tool for the verification of logic-based contracts refinement for embedded systems. It...
Read More
MathSAT – Modulo Theories Solver
MathSAT 5 is an efficient Satisfiability modulo theories (SMT) solver. MathSAT 5 is the...
Read More
RAT – Requirements Analysis Tool
The importance of requirements in the process of designing correct systems is being increasingly...
Read More
NUGAT – Game Solver
NuGaT is a game solver built on top of the NuSMV model checker.
Read More
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.
Read More
MBP: Model Based Planner
The Model Based Planner (MBP) is a system designed to perform plan synthesis, plan validation and...
Read More