Verification of neural networks:
CORA offers the verification of neural networks and neural-network controlled systems.
We provide the import of neural networks from various common machine learning frameworks via the ONNX format.
Improved ellipsoid class:
CORA now exploits degeneracy of sets to accelerate the computation and to improve the tightness of results.
Furthermore, we directly model all optimization problems for ellipsoidal operations
(requires either MOSEK or SDPT3 to be installed), which greatly improves runtime.
Hybrid systems extension:
The modeling capabilities for hybrid automata and parallel hybrid automata have been enhanced:
Reset functions can now depend on inputs and synchronization labels have been introduced.
Internal checks ensure the correctness of the CORA model.
Additionally, the spaceeex2cora converter has been extended to cover the new functionality
and updated display functions provide the user with a concise overview of a hybrid automaton on the command window.
Verification of temporal logic specifications:
Signal Temporal Logic formulae (STL) can be defined using the novel stl class.
This allows for a verification of STL formulae using Reachset Temporal Logic (RTL)
when STL objects are passed to reach functions as specifications.
Conversion of IEEE busses:
A new converter enables the conversion of IEEE busses to CORA models.
Miscellaneous:
Minor improvements have been made in various parts of the code:
Plot functions now support 1D projections, some basic functionality runs more efficiently,
standardized input argument validation and more accurate error messages
enhance the responsiveness, and more unit tests ensure greater reliability.