| Venus | 基于ReLU的前馈神经网络 | - 基于MILP求解器
- 支持生成反例 | 利用ReLU节点之间依赖关系，修剪基于MILP公式的验证问题的搜索树，大大缩短的验证过程的时间 | 只能应用于ReLU激活函数的神经网络 | Efficient Verification of ReLU-based Neural Networks via Dependency Analysis, 2020 |
| Marabou | 全连接神经网络和卷积神经网络 | - 基于SMT求解器，前身是Reluplex
- 支持生成反例 | 可以通过将查询转换为约束满足问题来回答关于网络属性的查询。它可以适应具有不同激活函数和拓扑结构的网络，并在网络上减少搜索空间，提高性能 | 只支持分段线性激活函数 | The Marabou Framework for Verification and Analysis of Deep Neural Networks, 2019 |
| Neurify | 全连接神经网络和卷积神经网络 | - 基于符号线性松弛和有向约束细化，在ReluVal上做出改进
- 支持生成反例 | 速度快，可以支持大型网络，生成反例的速度快 | 只针对ReLU激活函数进行讨论 | Efficient Formal Safety Analysis of Neural Networks, 2018 |
| NSVerify | 基于ReLU的前馈神经网络 | - 基于MILP求解器
- 把前馈神经网络表示成一个由agent和environment组成的系统
- 支持生成反例 | 建立了一种agent-environment系统的模型，其中agent是一组动作函数集合，environment是一组状态的集合。提供了一种语义，并开发了一种方法来自动验证系统在运行过程中是否达到了非预期的状态 | 只支持ReLU激活函数 | Reachability Analysis for Neural Agent-Environment Systems, 2018 |
| AI2 | 基于ReLU的前馈神经网络和卷积神经网络 | - 基于抽象解释
- 支持生成反例 | 用一组带条件的仿射函数来建模基于ReLU的神经网络，可以刻画神经网络中的全连接层、卷积层和最大池化层结构。 | 只支持ReLU激活函数 | AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation, 2018 |