Tools

  • NuSMV – Symbolic Model Checker

    NuSMV is a symbolic model checker developed as a joint project between: Embedded Systems Unit in the Center for Information Technology at FBK-IRST Model Checking group at Carnegie Mellon University, the Mechanized Reasoning Group at University of Genova Mechanized Reasoning Group at University of Trento NuSMV is a reimplementation and …

  • NuXMV

    nuXmv is a new symbolic model checker for finite- and infinite-state synchronous transition systems. nuXmv is the the eXtended version of NuSMV open source symbolic model checker. For further information, please refer to the nuXmv’s web page. Website

  • OCRA – Othello Contracts Refinement Analysis

    OCRA is a tool for the verification of logic-based contracts refinement for embedded systems. It supports the specification of components enriched with Othello contracts and the compositional verification of contracts refinement and implementation. It is built on top of the NuSMV model checker. We are glad to announce the availability …

  • xSAP – The Safety Analysis Platform

    xSAP is a tool for safety assessment of synchronous finite-state and infinite-state systems. It is based on symbolic model checking techniques. xSAP supersedes FSAP. Contacts Marco Bozzano

  • MathSAT – Modulo Theories Solver

    MathSAT 5 is an efficient Satisfiability modulo theories (SMT) solver. MathSAT 5 is the successor of MathSAT 4, supporting a wide range of theories (including e.g. equality and uninterpreted functions, linear arithmetic, bit-vectors, and arrays) and functionalities (including e.g. computation of Craig interpolants, extraction of unsatisfiable cores, generation …

  • NURV

    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 generate finite-state monitors into standalone monitor code in C, C++, Java, Python, Common Lisp, Prolog and LLVM …

  • 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 …

  • MBP: Model Based Planner

    The Model Based Planner (MBP) is a system designed to perform plan synthesis, plan validation and plan/domain simulation in non-deterministic domains. It provides: A general framework for modeling nondeterministic domains with various degrees of observability, and a language to support it. A general plan model, and a language supporting …

Contributed Tools

  • TASTE

    TASTE (The Assert Set of Tools for Engineering) is a tool-chain targeting heterogeneous embedded systems, using a model-based development approach, created under the initiative of the European Space Agency. TASTE can be used to design small to medium-size systems; it relies on formal languages and is based on the idea …

  • CHESS

    CHESS (Composition with Guarantees for High-integrity Embedded Software Components Assembly) tool is a open source software project that supports the design phases of safety-critical systems, combining the model-driven architecture design with formal methods. CHESS enable the interaction with external backend tools to perform different analysis. These external tools include OCRA …

  • Kratos

    Kratos is a software model checker for sequential and (cooperative) threaded C programs. Kratos verifies safety properties in the form of program assertion. For analysis of sequential programs, Kratos implements Lazy Predicate Abstraction (Blast algorithm) and Lazy Abstraction with Interpolants (McMillan/Impact algorithm) For analysis of threaded programs, Kratos implements …

  • 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 to the Verilog2SMV’s web page. Website

  • RAT – Requirements Analysis Tool

    The importance of requirements in the process of designing correct systems is being increasingly recognized. In the last years, several formalisms for describing requirements have been developed and made their way into the design process. PSL has been proposed as a means to write specifications that are both easy to …

  • NuGaT – Game Solver

    NuGaT is a game solver built on top of the NuSMV model checker.

Recent Posts