diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 967d8303d5f3af68fb9b52461a2d75654cf81613..4411d778c26d72c97e8555bd29c694ad4e1483bd 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -1,6 +1,6 @@
 variables:
-  CAISAR_VERSION: "1.0.0"
-  TAG: "1.0"
+  CAISAR_VERSION: "2.0.0"
+  TAG: "2.0"
 
 default:
   interruptible: true
@@ -20,7 +20,7 @@ build:
 # Optional and manual full rebuild using a clean docker image
 full_rebuild_and_test:
   stage: build
-  image: ocaml/opam@sha256:013a26ccbaa8344b63274e335e2492c432cec1c3526b9ba888ab151abb2b4c25
+  image: ocaml/opam:ubuntu-22.04-ocaml-4.13
   cache:
     key: $CI_COMMIT_REF_SLUG
     paths:
@@ -31,10 +31,11 @@ full_rebuild_and_test:
     - eval $(opam env --switch=4.13 --set-switch)
     - opam switch
     - sudo apt-get update
-    - sudo apt install -y protobuf-compiler
+    - sudo apt-get install -y protobuf-compiler python3 python3-pip cmake
     - opam repository add remote https://opam.ocaml.org
     - opam depext --yes ocplib-endian base fmt alt-ergo.2.4.0
     - opam install --jobs 2 . --deps-only --with-test --yes
+    - python3 -m pip install onnx
     - make all-ci
     - make test-ci
   tags:
diff --git a/CHANGES.md b/CHANGES.md
index a96840ea3b060fa3d937882675c867af83cd12c1..d848ead7121ba16a792d6e6805db6fd72e38d4ab 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,3 +1,64 @@
+# 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
diff --git a/doc/conf.py b/doc/conf.py
index 2e45e7bca5698da02cd44e90464083b17412fe62..e7f85be9bebfee6103e169fa5e229a6bfefbac7c 100644
--- a/doc/conf.py
+++ b/doc/conf.py
@@ -21,7 +21,7 @@ sys.path.append(os.path.abspath('./ext'))
 # -- Project information -----------------------------------------------------
 
 project = 'CAISAR'
-copyright = '2023, The CAISAR Development Team'
+copyright = '2024, The CAISAR Development Team'
 author = 'The CAISAR Development Team'
 
 # The version info for the project you're documenting, acts as replacement for
@@ -29,9 +29,9 @@ author = 'The CAISAR Development Team'
 # built documents.
 #
 # The short X.Y version.
-version = '1.0'
+version = '2.0'
 # The full version, including alpha/beta/rc tags.
-release = '1.0'
+release = '2.0'
 
 
 # -- General configuration ---------------------------------------------------
diff --git a/doc/contributing.rst b/doc/contributing.rst
index cc1d17a088ea5fcaffb3f85a12ad3ddb6a54acf4..76d8393590ac30299ba1b013d261cdf8a38cb211 100644
--- a/doc/contributing.rst
+++ b/doc/contributing.rst
@@ -27,6 +27,7 @@ The root of the repository has the following folders:
 * ``stdlib/`` contains WhyML files used to define
   theories for the CAISAR interpreted language.
 * ``tests/`` are non-regression tests written in `dune cram test syntax <https://dune.readthedocs.io/en/stable/tests.html>`_.
+* ``utils/`` are helper functions used internally by CAISAR (for instance, logging utilities).
 
 
 Setting up a development environment
diff --git a/doc/index.rst b/doc/index.rst
index 6ccf4ea49a075e96962f7bffede89ecbb5ac1836..00bcd02007b37f8a5400faeb365f3bb1a3238017 100644
--- a/doc/index.rst
+++ b/doc/index.rst
@@ -18,12 +18,13 @@ The CAISAR Platform
   François Bobot,
   Julien Girard
 
-:Version: |version|, December 2023
-:Copyright: 2020--2023 CEA (Commissariat à l'énergie atomique et aux énergies alternatives)
+:Version: |version|, June 2024
+:Copyright: 2020--2024 CEA (Commissariat à l'énergie atomique et aux énergies alternatives)
 
 .. _Confiance.ai: https://www.confiance.ai/
+.. _DeepGreen: https://www.deepgreen.ai/
 
-This work has been partly supported by the `Confiance.ai`_ program.
+This work has been partly supported by the `Confiance.ai`_ program and the `DeepGreen`_ project.
 
 .. toctree::
    :maxdepth: 2
diff --git a/doc/interpretation.rst b/doc/interpretation.rst
index f484ad314b1e53a5b9e726711c8afefccd99dbb9..b87e9b1f6b0d549392c877a186470595fb94762c 100644
--- a/doc/interpretation.rst
+++ b/doc/interpretation.rst
@@ -109,12 +109,12 @@ Functions
 
 .. code-block:: whyml
 
-  (** Returns a symbol for the neural network with filename n. **)
-  function read_model (n: string) : model nn
+  (** Returns a symbol for the machine learning model with filename n. **)
+  function read_model (n: string) : model
 
-  (** Returns a vector that represents the application of neural network
+  (** Returns a vector that represents the application of a model
   on an input vector. **)
-  function (@@) (n: model nn) (v: vector 'a) : vector 'a
+  function (@@) (n: model) (v: vector 'a) : vector 'a
 
 Dataset
 *******
diff --git a/docker/Dockerfile.template b/docker/Dockerfile.template
index 47d4a2f76ac5e41984ee295f8b3a0a867c5d632e..122bb09e6e4c1e8528211ca8fe3a09cc1375f47a 100644
--- a/docker/Dockerfile.template
+++ b/docker/Dockerfile.template
@@ -76,6 +76,10 @@ cmake --build .
 
 ENV PATH "/home/opam/Marabou/build:$PATH"
 
+## Maraboupy
+
+RUN /usr/bin/python3.10 -m pip install maraboupy
+
 ## SAVer
 
 RUN git clone https://github.com/svm-abstract-verifier/saver.git && \
diff --git a/flake.nix b/flake.nix
index 64f7be9a6eb472cf3c38f9dc9afe0191776ce14c..d4cb8c8ab752fa0f0cb1d3098d7ac95d1cd938ab 100644
--- a/flake.nix
+++ b/flake.nix
@@ -43,7 +43,7 @@
         caisar = ocamlPkgs.buildDunePackage
           {
             pname = "caisar";
-            version = "1.0.0";
+            version = "2.0.0";
             duneVersion = "3";
             minimalOCamlVersion = "4.13";
             installTargets = "all doc";