diff --git a/doc/_static/media/acas_xu.png b/doc/_static/media/acas_xu.png
new file mode 100644
index 0000000000000000000000000000000000000000..d6de240a4a6fc470fc6a321de10ecc4a2a25ba17
Binary files /dev/null and b/doc/_static/media/acas_xu.png differ
diff --git a/doc/acas_xu.rst b/doc/acas_xu.rst
new file mode 100644
index 0000000000000000000000000000000000000000..8baa5b519540bb918fa39575a915351d01b0bf2f
--- /dev/null
+++ b/doc/acas_xu.rst
@@ -0,0 +1,236 @@
+.. _acas_xu:
+
+ACAS-Xu
+*******
+
+ACAS-Xu stands for Aircraft Collision Avoidance System.
+Introduced for instance in [Manfredi2016]_, it is a
+specification of a program which aim to output signals for
+an aircraft in a situation where there is a potential for
+collision.
+In the rest of this tutorial, we will use the flavour
+ACAS-Xu defined in [Katz2017]_, where the authors aim to
+verify a neural network implementing part of the ACAS-Xu
+specification.
+Its low dimensionality and well defined semantics
+make it a *de facto* benchmark for machine learning
+verification.
+
+Use-case presentation
+=====================
+
+The system considers a 2D plane with two entities: the
+monitored plane (the "ownship") and an incoming plane (the "intruder").
+
+.. image:: _static/media/acas_xu.png
+ :alt: A picture with two aircrafts seen from above
+
+In the original implementation, the system state has seven
+inputs:
+
+* :math:`v_{own}`: speed of ownship
+* :math:`v_{int}`: speed of intruder
+* :math:`\rho`: distance from ownship to intruder
+* :math:`\theta`: angle to intruder relative to ownship heading direction
+* :math:`\psi`: heading angle of intruder relative to ownship heading direction
+* :math:`\tau`: time until vertical separation
+* :math:`a_{prev}`: previous advisory
+
+It has five outputs, that correspond to the different
+direction advisories the system can give:
+
+* :math:`COC`: Clear Of Conflict
+* :math:`WL`: Weak Left
+* :math:`SL`: Strong Left
+* :math:`WR`: Weak Right
+* :math:`SR`: Strong Right
+
+In the paper, the authors are producing multiple neural
+network that correspond to several values of :math:`\tau`
+and :math:`a_{prev}`, producing an array of 45 neural
+networks, with only five inputs (and the same number of
+outputs). We will consider five-inputs network in the
+future.
+
+Properties
+----------
+
+There are several functional properties one may want to verify on this system, for instance:
+
+* guarantee that the system will never output COC advisory when the intruder is nearby
+* guarantee that the system will never output an advisory that may result in a collision
+* guarantee that the system will not output a Strong advisory where a Weak variant would be enough
+
+Authors of [Katz2017]_ propose ten properties to verify. We
+will reproduce the first here, and try to check whether a
+given neural network respects it.
+
+**property**
+ :math:`\phi_1`
+
+**definition**
+ If the intruder is distant and is significantly slower than the ownship, the score of a COC advisory will always be below a certain fixed threshold.
+
+**input constraints**
+
+ * :math:`\rho` ≥ 55947.691
+ * :math:`v_{own}` ≥ 1145
+ * :math:`v_{int}` ≤ 60
+
+**desired output property**
+
+ * :math:`COC` ≤ 1500
+
+Modelling the problem using WhyML
+---------------------------------
+
+The first step for verifying anything with CAISAR is to
+write a WhyML file that describe the problem to solve.
+Inside this file, we will create a *theory*. A theory can be
+seen as a namespace inside CAISAR, inside which are defined logical terms,
+formulas and verification goals.
+
+Let us try to model the property :math:`\phi_1` defined
+earlier. We will call our theory `ACAS_XU_P1`.
+
+.. code-block:: ocaml
+
+ theory ACAS_XU_P1
+ end
+
+We will need to write down some numerical values. As of now,
+CAISAR support writting values using floating point arithmetic.
+Why3 defines a float type and the relevant arithmetic
+operations according to the IEEE floating
+point standard in a theory, astutely called ``ieee_float``.
+Specifically, we will import the ``Float64`` subtheory, that
+defines everything we need for 64 bit precision floating
+point numbers.
+We thus import it in our theory using the ``use`` keyword.
+
+Our file looks like this so far:
+
+.. code-block:: ocaml
+
+ theory ACAS_XU_P1
+ use ieee_float.Float64
+ end
+
+We would like to verify our propety given a certain neural network.
+To do this, we can write the filename in our theory.
+Internally, when provided with a neural network file, CAISAR will perform some basic sanity checks (mainly, checks that the network is in a supported format).
+If those checks pass, then CAISAR will internally build a theory, named as the original neural network. This theory will contain two subtheories that provide
+logical symbols we can use in our theory: ``AsTuple`` and ``AsArray``.
+We will only consider the ``AsTuple`` subtheory for this tutorial.
+
+This theory is equivalent to the following WhyML file:
+
+.. code-block:: ocaml
+
+ theory Name_of_neural_network_file
+ theory AsTuple
+ type t
+ (* Tuple with as many elements as there are input *)
+ function nn_apply (t,_,...)
+ (* Tuple with as many elements as there are outputs *)
+ : (t,_,...)
+ end
+ (* Other stuff *)
+ end
+
+CAISAR defines the ``AsTuple`` theory, inside which there is a
+``nn_apply`` function symbol. The input of this function as a tuple with
+as many elements as there are inputs on the original neural network,
+and return a tuple with as many elements as there are outputs
+original neural network.
+
+As our neural network takes five inputs and five outputs, by
+adding ``use filename.AsTuple`` will provide a ``nn_apply``
+function symbol that takes a 5-elements tuple as input, and output
+a 5-element tuple. Supposing we have a neural network named
+*ACAS_XU_P1.nnet*, our file looks like this:
+
+.. code-block:: ocaml
+
+ theory ACAS_XU_P1
+ use ACASXU_1_1.AsTuple
+ use ieee_float.Float64
+ end
+
+Now is the time to define our verification goal ``G``.
+
+We first define constraints on our inputs, as defined in
+property :math:`\phi_1`. We define all floating points inputs
+:math:`x_i` for :math:`i \in (0..4)` that respect the
+properties defined in :math:`\phi_1` (in WhyML, ``->`` stands for
+the logical implication).
+
+.. code-block:: ocaml
+
+ goal G: forall x0 x1 x2 x3 x4.
+ (0.5999999999999999777955395074968691915273666381835937500000000000:t) .<= x0 .<= (0.6798577687000000313588543576770462095737457275390625000000000000:t) ->
+ (-0.5:t) .<= x1 .<= (0.5:t) ->
+ (-0.5:t) .<= x2 .<= (0.5:t) ->
+ (0.4500000000000000111022302462515654042363166809082031250000000000:t) .<= x3 .<= (0.5:t) ->
+ (-0.5:t) .<= x4 .<= (-0.4500000000000000111022302462515654042363166809082031250000000000:t) ->
+
+Then, whe define the result of the application of ``net_apply`` on the inputs as the following, taking advantage of the pattern-matching of WhyML, and define
+the output constraint we want to enforce.
+
+.. code-block:: ocaml
+
+ let (y0, _, _, _, _) = nn_apply x0 x1 x2 x3 x4 in
+ y0 .< (3.9911256458999999630066213285317644476890563964843750000000000000:t)
+
+The final file looks like this:
+
+.. code-block:: ocaml
+
+ theory ACAS_XU_P1
+ use ACASXU_1_1.AsTuple
+ use ieee_float.Float64
+
+ goal G: forall x0 x1 x2 x3 x4.
+ (0.5999999999999999777955395074968691915273666381835937500000000000:t) .<= x0 .<= (0.6798577687000000313588543576770462095737457275390625000000000000:t) ->
+ (-0.5:t) .<= x1 .<= (0.5:t) ->
+ (-0.5:t) .<= x2 .<= (0.5:t) ->
+ (0.4500000000000000111022302462515654042363166809082031250000000000:t) .<= x3 .<= (0.5:t) ->
+ (-0.5:t) .<= x4 .<= (-0.4500000000000000111022302462515654042363166809082031250000000000:t) ->
+ let (y0, _, _, _, _) = nn_apply x0 x1 x2 x3 x4 in
+ y0 .< (3.9911256458999999630066213285317644476890563964843750000000000000:t)
+ end
+
+This file is available as is, under the example folder of our repo: `property_1.why <https://git.frama-c.com/pub/caisar/-/blob/master/examples/acasxu/property_1.why>`_.
+A neural network in NNet format that should respect this
+property is available here: `ACASXU_1_1.nnet <https://git.frama-c.com/pub/caisar/-/blob/master/examples/acasxu/nets/https://git.frama-c.com/pub/caisar/-/blob/master/examples/acasxu/nets/ACASXU_1_1.nnet>`_ (from the Marabou repository).
+
+
+Checking the property with CAISAR
+---------------------------------
+
+Assuming the chosen prover is on your path and you are in
+CAISAR's root, you may launch caisar using the following command line:
+
+
+.. code-block:: bash
+
+ caisar verify --prover Marabou -L examples/acasxu/nets/ --format whyml examples/acasxu/property_1.why -vv -t 10m
+
+Take note that this may take some time, depending to your
+machine.
+
+CAISAR will return you either ``Valid``, ``Invalid`` or
+``Timeout``
+
+
+
+References
+----------
+
+
+.. [Manfredi2016] G. Manfredi and Y. Jestin, "An introduction
+ to ACAS Xu and the challenges ahead," 2016 IEEE/AIAA
+ 35th Digital Avionics Systems Conference (DASC),
+ 2016, pp. 1-9, doi: 10.1109/DASC.2016.7778055.
+
+.. [Katz2017] Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J. (2017). Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. In: Majumdar, R., KunÄak, V. (eds) Computer Aided Verification. CAV 2017. Lecture Notes in Computer Science(), vol 10426. Springer, Cham. https://doi.org/10.1007/978-3-319-63387-9_5
diff --git a/doc/conf.py b/doc/conf.py
index 1eff397760cee828038f42fcb8bb3c778f106bac..b3991ef3949154f321b22bc44d3919e31d562080 100644
--- a/doc/conf.py
+++ b/doc/conf.py
@@ -49,4 +49,4 @@ html_theme = 'alabaster'
# Add any paths that contain custom static files (such as style sheets) here,
# relative to this directory. They are copied after the builtin static files,
# so a file named "default.css" will overwrite the builtin "default.css".
-html_static_path = ['_static']
\ No newline at end of file
+html_static_path = ['_static']
diff --git a/doc/contents.rst b/doc/contents.rst
deleted file mode 100644
index daa46db69729e3f5b7d11b30c01926ca8b00c326..0000000000000000000000000000000000000000
--- a/doc/contents.rst
+++ /dev/null
@@ -1,10 +0,0 @@
-Table of content
-================
-
-.. toctree::
- :maxdepth: 2
- :caption: Contents:
-
- installation
- usage
- modules
diff --git a/doc/examples.rst b/doc/examples.rst
new file mode 100644
index 0000000000000000000000000000000000000000..028911d28dd0196703d12e64e9ad6de1ab3a1d43
--- /dev/null
+++ b/doc/examples.rst
@@ -0,0 +1,14 @@
+.. _examples:
+
+Examples
+========
+
+This page regroups some examples use cases for CAISAR. All
+examples will describe the use case, the formalization using
+WhyML, and the CAISAR execution.
+
+.. toctree::
+ :maxdepth: 2
+ :caption: Examples:
+
+ acas_xu
diff --git a/doc/index.rst b/doc/index.rst
index 7a26e02ada6f54db0dce86889e8a1ab5b1a7fa87..17d89bb3fd1fa936f075204ae328a0f7154667c1 100644
--- a/doc/index.rst
+++ b/doc/index.rst
@@ -26,6 +26,7 @@ Content
installation
usage
+ examples
modules