CORA

The Continuous Reachability Analyzer (CORA) is a collection of MATLAB classes for the formal verification of cyber-physical systems using reachability analysis. CORA integrates various vector and matrix set representations and operations on them as well as reachability algorithms of various dynamic system classes. The software is designed such that set representations can be exchanged without having to modify the code for reachability analysis.

Main features:

• Reachability analysis of linear systems, nonlinear systems as well as systems with constraints in continuous and discrete time.
• Reachability analysis of hybrid systems, including multiple different methods for the calculation of the intersections with guard sets.
• Set-based computing using various vector set representations, e.g., intervals, zonotopes, Taylor models, and polytopes, as well as matrix set representations, such as matrix zonotopes and interval matrices.
• Formal verification of neural networks, both in open-loop as well as in closed loop scenarios.

For more details, please refer to the CORA website.