Automatic system identification:
It is now possible to automatically identify a suitable dynamic model from data and establish reachset conformance via the \(\texttt{identify}\) and \(\texttt{conform}\) operators. We also overhauled how trajectories are handled in CORA to improve efficiency. For details, please visit Sec. 4.1.9, Sec. 4.1.11, and Sec. 7.2.
Neural network verification:
We significantly improved the verification of neural networks in CORA, added the ability to verify graph neural networks, generate sufficient explanations for neural network predictions, and overhauled the training of verifiably robust neural networks. Details can be found in Sec. 6.
Set containment certificate:
While \(\texttt{contains}\) has always returned \(\texttt{true}\) if CORA was able to determine containment, a returned \(\texttt{false}\) might also indicate that containment holds, but CORA is not able to determine it. To eliminate this ambiguity, \(\texttt{contains}\) now also returns a certificate on the result. Details are described in Sec. 2.1.2.1.
Visualizations:
We revised the plotting capabilities of CORA and introduced a new default schema to plot sets to improve visibility on small monitors and beamers. It is also possible to create animated videos directly from CORA. Additionally, users might want to check \(\texttt{CORAtable}\)s for better display of tabular data. For details, please visit Sec. 2.1.4.10.
Repeatability package:
If you want to use CORA as part of a repeatability package, we got you covered and provide a Docker file with all dependencies installed. Instructions on how to set it up can be found in Appendix F.
Miscellaneous:
Minor improvements have been made in various parts of the code: Some basic functionality runs more efficiently, several bug fixes result in an improved user experience, and more unit tests ensure greater reliability. Please also have a look at Appendix A.12 for deprecated functionality and their replacements.