You are here
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.
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.
NuSMV is a symbolic model checker and is a reimplementation and extension of SMV, the first model checker based on BDDs.
NuSMV has been designed to be an open architecture for model checking, which can be reliably used for the verification of industrial designs, as a core for custom verification tools, as a testbed for formal verification techniques, and applied to other research areas.
OCRA is a tool for the verification of logic-based contracts refinement for embedded systems.
MathSAT is an efficient Satisfiability modulo theories (SMT) solver. MathSAT supports 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 of models and proofs, and the ability of working incrementally).
RAT (Requirements Analysis Tool) is a tool supporting a methodology to pinpoint defects in a set of requirements specifying the expected behavior of the new system.
Kratos is a software model checker for sequential and (cooperative) threaded C programs. Kratos verifies safety properties in the form of program assertion.
NuGaT is a game solver built on top of the NuSMV model checker.