[release] Update changelog

CHANGES.md

+# 2.0 (17-06-2024)
+
+- [interpretation] Add transformations that allow the verification of several
+  neural network at once. Within particular patterns, CAISAR will generate
+  an ONNX file that preserve the semantic of the neural networks
+  while encapsulating parts of the
+  specification directly in the control flow of the neural network.
+  This feature allow the verification of properties with multiple neural
+  networks, including their composition.
+
+- [interpretation] Integrate SVMs into the interpretation engine. Users can
+  expect vector computations and applications on SVMs to be computed similarly
+  as what exists already for neural networks.
+
+- [interpretation] Add support for addition between vectors.
+
+- [interpretation] Add better error reporting for interpretation errors. Users
+  now get better guidance on how to write their specification. For instance,
+  CAISAR now explicitly asks for a predicate constraining the length of a vector
+  after a universal quantifier.
+
+- [language] Unified Support Vector Machines (SVMs) theories.
+  Previously, there was a separate theory for neural networks and SVMs datasets
+  and models. They are now accessible under a single theory.
+
+- [language] Add additional abstraction support for SVMs.
+
+- [language] Simplify CAISAR's Neural Intermediate Representation (NIR) and
+  perform automatic shape inference when creating a new NIR node.
+
+- [language] Add support for the following ONNX operators: `Gather`, `Log`, `Abs`,
+  `RandomNormal`, `ReduceSum`.
+
+- [language] Neural networks in NNet format are now parsed into a NIR.
+
+- [examples] Rework ACAS-Xu specification with a formulation that is closer to
+  the original. In particular, provide explicit normalization and
+  denormalization functions in the test file. Also define explicit function
+  contracts using Why3 pre and post-conditions.
+
+- [examples] Add more examples displaying CAISAR ability to handle several
+  neural networks at once.
+
+- [cmdline] Add command line option `--onnx-out-dir`
+  to output the NIR generated by CAISAR as an ONNX file.
+
+- [logging] Add command line option `--ltag` for fine-grained logging.
+  By providing a logging tag (`ltag`), users can control which part of CAISAR
+  will log its outputs.
+
+- [prover] Add support for Marabou 2.0 via its Python API. Autodetection of
+  Marabou installed through maraboupy is now supported.
+
+- [prover] Update AIMOS configuration to match upstream.
+
+- [prover] Update $\alpha-\beta-$CROWN configuration to match upstream.
+
+- [doc] Clarify the supported ONNX operator set: the ONNX Intermediate
+  Representation is version 8, the supported operator set is version 13.
+
+
 # 1.0 (08-12-2023)
 
 - [language] Extended WhyML for AI systems. It is now possible to model with