Veritex is a Python toolbox for verification and automated repair
of Deep Neural Networks. The tool enables:
TLTk is a modular tool for parallel robustness computation of
Signal Temporal Logic (STL) specifications. At the core of the
tool, an algorithm for robustness computation is utilized that
supports multi-threaded CPU/GPU computation. . The tool enables
parallel robustness computation of large traces. In addition, the
python implementation enables the addition and modification of
temporal operators for application-specific scenarios
S-TaLiro is a suite of tools for testing and verification of
Cyber-Physical Systems. It is a toolbox for Matlab/Simulink. It
enables the analysis of continuous and hybrid dynamical systems
using temporal logics.
The main features of S-TaLiRo include:
S-TaLiRo has been applied to numerous challenging applications
from the automotive and medical device industries. To download or
learn more visit the
. The DIFTS2014
provides a good overview of the tool and its features.
In 2012 and 2014, S-Taliro was nominated as a technological
breakthrough by the industry! (Read the report
One of the main barriers preventing widespread use of formal
methods is the elicitation of formal specifications. ViSpec is a
graphical tool designed for the development and visualization of
formal specifications by people that do not have training in
formal logic. The tool enables users to develop specifications
using a graphical formalism which is then automatically translated
to Metric Temporal Logic (MTL). .
to download the software. Update coming soon...