The Why3 Platform
=================

:Authors:
  François Bobot,
  Jean-Christophe Filliâtre,
  Claude Marché,
  Guillaume Melquiond,
  Andrei Paskevich

:Version: |version|, April 2024
:Copyright: 2010--2024 University Paris-Saclay, CNRS, Inria

.. _U3CAT: http://frama-c.com/u3cat/
.. _Hi-Lite: http://www.open-do.org/projects/hi-lite/
.. _BWare: http://bware.lri.fr/
.. _ProofInUse: http://www.spark-2014.org/proofinuse
.. _CoLiS: http://colis.irif.univ-paris-diderot.fr/
.. _VOCal: https://vocal.lri.fr/

This work has been partly supported by the `U3CAT`_ national ANR project
(ANR-08-SEGI-021-08), the `Hi-Lite`_ FUI project of the System\@tic
competitivity cluster, the `BWare`_ ANR project (ANR-12-INSE-0010), the
Joint Laboratory `ProofInUse`_ (ANR-13-LAB3-0007), the `CoLiS`_ ANR
project (ANR-15-CE25-0001), and the `VOCaL`_ ANR project
(ANR-15-CE25-008).

.. toctree::
   :maxdepth: 3
   :numbered:

   foreword
   starting
   whyml
   install
   manpages
   syntaxref
   input_formats
   vcgen
   exec
   itp
   api
   technical
   changes
   zebibliography
   genindex

.. * :ref:`genindex`
.. * :ref:`search`
.. * :ref:`modindex`