CORA

Toolbox for Reachability Analysis

The Continuous Reachability Analyzer (CORA) is a MATLAB-based toolbox designed for the formal verification of cyber-physical systems through reachability analysis. It offers a comprehensive suite of tools for modeling and analyzing various system dynamics, including linear, nonlinear, and hybrid systems. CORA supports both continuous and discrete-time systems, accommodating uncertainties in system inputs and parameters. These uncertainties are captured by a diverse range of set representations such as intervals, zonotopes, Taylor models, and polytopes. Additionally, CORA provides functionalities for the formal verification of neural networks as well as data-driven system identification with reachset conformance. Various converters are implemented to easily model your system in CORA such as the well-established SpaceEx format for dynamic systems and ONNX format for neural networks. CORA ensures the seamless integration of different reachability algorithms without code modifications and aims for a user-friendly experience through automatic parameter tuning, making it a versatile tool for researchers and engineers in the field of cyber-physical systems.