overview.md

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:

• The tool is supported by DNNV.
• The tool lists its dependencies in setup.py and README.md, but does not list version bounds.

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 only compatible with Ubuntu 22.04.
• 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.