[doc] Added dedicated page to supported provers

doc/foreword.rst

@@ -35,19 +35,12 @@ needed to interoperate with external provers. These are generally called
 Supported Provers
 -----------------
 
-The supported provers are the following:
-
-* `PyRAT <https://laiser.frama-c.com/laiser-websites/pyrat-website/>`_, a neural
-  network prover based on abstract interpretation,
-* `Marabou <https://github.com/NeuralNetworkVerification/Marabou>`_, a
-  Satisfiability Modulo Theory (SMT) solver specialized in neural network
-  verification,
-* `SAVer <https://github.com/abstract-machine-learning/saver>`_, a support
-  vector machine prover based on abstract interpretation,
-* `nnenum <https://github.com/stanleybak/nnenum>`_, a neural network prover
-  that combines abstract interpretation and linear programming techniques,
-* `alpha-beta-CROWN <https://github.com/Verified-Intelligence/alpha-beta-CROWN>`_, a neural network prover, winner of the VNN-COMP 2021 and 2022,
-* Standard SAT/SMT solvers that support the SMT-LIBv2 input language.
+.. toctree::
+   :maxdepth: 2
+   :caption: Supported Provers:
+
+   provers
+
 
 Availability
 ------------
@@ -79,9 +72,6 @@ We gratefully thank the people who contributed to CAISAR, directly or
 indirectly: Zakaria Chihani, Serge Durand, Tristan Le Gall, Augustin Lemesle,
 Aymeric Varasse.
 
-Bibliography
-------------
-
 .. [GABC2023] Girard-Satabin, J., Alberti, M., Bobot, F., Chihani, Z.,
               *Caractériser des propriétés de confiance d’IA avec Why3*,
               Journées Francophones des Langages Applicatifs (J FLA 2023)

doc/provers.rst

+
+The supported provers are the following:
+
+PyRAT
+-----
+`PyRAT <https://pyrat-analyzer.com>`_
+is a neural network prover based on abstract interpretation,
+
+Marabou
+-------
+`Marabou <https://github.com/NeuralNetworkVerification/Marabou>`_
+is a Satisfiability Modulo Theory (SMT) solver specialized in neural network
+verification.
+
+SAVer
+-----
+`SAVer <https://github.com/abstract-machine-learning/saver>`_
+is a support vector machine prover based on abstract interpretation.
+
+nnenum
+------
+
+`nnenum <https://github.com/stanleybak/nnenum>`_ is a neural network prover that combines abstract interpretation, linear programming techniques and input split heuristics.
+
+alpha-beta-CROWN
+--------------------------
+
+`alpha-beta-CROWN <https://github.com/Verified-Intelligence/alpha-beta-CROWN>`_ is a neural network prover, winner of the VNN-COMP 2021 and 2022.
+
+SMT solvers
+-----------
+Standard SAT/SMT solvers that support the SMT-LIBv2 input language.
+As of now, only CVC5 had been tested.

doc/usage.rst

@@ -21,7 +21,7 @@ refer to each prover documentation to install them.
 
 CAISAR
 already support several provers, listed in
-:ref:`overalldesign`.
+:ref:`supported-provers`.
 Assuming you have installed a prover with an entry in the
 ``caisar-detection.conf`` file, you can register the prover to CAISAR using the
 following command: ``PATH=$PATH:/path/to/solver/executable caisar config -d``.
@@ -40,7 +40,7 @@ documentation to get a first grasp on using WhyML.
 
 Provided a file ``trust.why`` containing a goal to verify, the command ``caisar verify --prover=PROVER trust.why``
 will verify the goals using the specified prover. A list of
-supported provers is available in :ref:`overalldesign`. The prover
+supported provers is available in :ref:`supported-provers`. The prover
 must already be registered by CAISAR. Currently, only one
 prover can be selected at a time; future work will allow
 selecting multiple provers and orchestrate verification