.. _provers:

Supported provers
*****************

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.


.. warning ::
   Marabou and VNN-LIB provers (nnenum, alpha-beta-CROWN) do not accept strict
   inequalities. Thus CAISAR treats strict inequalities as non-strict ones. We
   are aware that this is not correct in general, but it is the current common
   practice in the community.