Verifier Backends
This page lists supported and possible future verifier backends, and relevant information about them.
Supported
Marabou
Further information:
The tool is supported by DNNV.
The tool has continuous integration on GitHub Actions.
The tool lists its dependencies in README.md
Under consideration
auto_LiPRA
Further information:
The tool has no continuous integration.
The tool lists its dependencies in setup.py.
The tool is distributed on PyPI.
BaB
Further information:
DNNV
Further information:
The tool has continuous integration on GitHub Actions.
The tool lists its dependencies in pyproject.toml.
The tool is distributed on PyPI.
ERAN
Further information:
The tool is supported by DNNV.
The tool has no continuous integration.
The tool lists its dependencies in requirements.txt.
The tool requires proprietary software (Gurobi).
MIPVerify.jl
Further information:
The tool is supported by DNNV.
The tool has continuous integration on GitHub Actions.
The tool lists its dependencies in Project.toml.
nnenum
Further information:
The tool is supported by DNNV.
The tool has continuous integration on Travis.CI.
The tool lists its dependencies in requirements.txt.
The tool has a Dockerfile.
NNV
Further information:
The tool has no continuous integration.
The tool requires proprietary software (MatLab).
The tool lists its requirements in README.md.
Neurify
Further information:
The tool is supported by DNNV.
The tool has no continuous integration.
The tool lists is requirements in README.md.
OVAL
Further information:
The tool has no continuous integration.
The tool lists its requirements in setup.py, but does not list version bounds.
Planet
Further information:
The tool is supported by DNNV.
The tool lists its requirements in README.md, but only as packages for Ubuntu 17.04.
QNNVerifier
Further information:
The tool has no continuous integration.
The tool lists its requirements in README.md, but does not list version bounds.
VeriNet
Further information:
The tool is supported by DNNV.
The tool has no continuous integration.
The tool lists its requirements in Pipfile, but does not list version bounds.
The tool lists exact versions for its requirements in Pipfile.lock
Rejected
α,β-CROWN
Further information:
The tool has no continuous integration.
The tool lists its requirements in requirements.txt
The tool is not distributed on PyPI and has no setup.py script.
Reasons for Rejection on 2023-04-14:
Limited compatibility, no versioning or distribution.
CROWN
Further information:
The repository is mirrored at huanzhang12/CROWN-Robustness-Certification.
The tool has no continuous integration.
The tool does not list its dependencies.
Reasons for Rejection on 2023-04-14:
Unmaintained and deprecated in favour of auto_LiPRA.
Reluplex
Further information:
The tool is supported by DNNV.
The tool has no continuous integration.
The tool lists its dependencies in README.txt.
Reasons for Rejection on 2023-04-14:
Unmaintained and deprecated in favour of Marabou.