# PV4 ⊧ NNV: Neural Network Verificationchecks whether the given network is safe

Set-based verification framework for deep neural networks (DNNs) and learning-enabled cyber-physical systems (CPS).### Application domain/field

- Neural network
- Deep neural networks
- Neural network verification

### Type of tool

Neural network verifier### Expected input

- Network configuration
- Plant configuration

Format:

? (it is a toolbox for Matlab)### Expected output

`SAT`

or `UNSAT`

which indicates whether the network is safe, i.e. the reachable sets do not violate any of the safety properties.
If the network is unsafe then it will provide a complete set of counter-examples that show all possible unsafe initial inputs and states.
It is possible for the tool to report `UNK`

in case the result is unknown.
### Internals

- NNV consists of a set of reachability algorithms that can be used to reason about deep neural networks (DNNs), specifically for
*sequential*FFNNs (feed forward neural networks) and CNNs (convolutional neural networks), as well as NNCS (neural network control systems) with FFNN controllers. - These reachability algorithms can be used to compute exact and over-approximate reachable sets of DNNs and neural network control systems (NNCSs).