CoVerNet: Toward Coverage Testing for Neural Networks Based on Formally Verified Equivalence Classes
Neural networks (NNs) are increasingly deployed in safety-critical systems such as automotive and medical devices, where failures can lead to severe consequences. This necessitates rigorous and effective testing. However, traditional coverage metrics such as neuron coverage which is adapted from software testing, often fails to reflect the adequacy of a test suite in detecting unintended behaviors. High neuron coverage does not necessarily imply effective fault detection. To address these limitations, we propose CoVerNet, a novel NN testing approach with a new test criterion called behavioral coverage. Unlike existing metrics, behavioral coverage is strongly correlated with the model’s decision space and more accurately identifies untested regions. CoVerNet clusters the input space into equivalence classes and leverages formal verification with Marabou, guaranteeing that each equivalence class exhibits similar behavior. It then explores each region iteratively, expanding them until counterexamples are found. CoVerNet is evaluated on different use cases including the IRIS multi-class classification task and ADIMA, an automated peripheral detection system. In addition, the applicability of CoVerNet approach is assessed on two synthetic use cases. The conducted experiments and obtained results demonstrate that behavioral coverage effectively guides test generation, identifies hidden vulnerabilities, and reflects test adequacy more effectively than neuron coverage
This is the official beta implementation accompanying the paper:
Authors: Yassine Akhiat, Zamira Daw
Implementation: Rochdi Dardor, Yassine Akhiat
Affiliation: Institute of Aircraft Systems (ILS) | University of Stuttgart | Germany
Published in: IEEE DASC 2025
DOI: https://doi.org/10.1109/DASC66011.2025.11257196
CoVerNet/
├── config/
│ └── default.yml
├── src/
│ ├── Algo.py # Main algorithm
│ ├── BehavioralCoverage.py
│ ├── Clustering.py
│ ├── FormalVerifier.py # Marabou integration
│ ├── FormPECs.py
│ ├── PropertyManager.py
│ └── __init__.py
├── onnx/ # Example models (IRIS, ADIMA, synthetic)
├── properties/ # Generated .prop files + results
├── requirements.txt
├── LICENSE
└── README.md- Formal verification of input regions using Marabou
- Behavioral Coverage (
Bc) — new and meaningful coverage metric - Finds bugs missed by 100% neuron coverage
- Scalable: iterative ε-expansion + cluster subdivision
git clone https://github.com/yourusername/CoVerNet.git
cd CoVerNet
python -m venv venv
source venv/bin/activate # Windows: venv\Scripts\activate
pip install -r requirements.txt
# ensure Marabou solver deps are installed, if not run this command
pip install maraboupy python -m src.Algo --config config/default.yml
This runs the full CoVerNet pipeline and prints something like:
Behavioral Coverage (B_C): 62.5%
Verified Equivalence Classes (VECs): 5 / 8
Counterexamples found in 3 clusters (SAT)
Results saved → properties/prop_c[N]_[N]_[mode].txtThis runs the full CoVerNet pipeline using the single config file and prints coverage and verification results. Outputs are written under properties/.
- model_path: ONNX model path.
- output_dir: Destination for generated property files/results.
- verification:
initial_epsilon,delta_epsilon,max_depth,timeout_seconds. - subdivision:
min_samplesfor reclustering suspect regions. - data:
npz_pathto dataset (X,yexpected); falls back to IRIS data for testing if empty;already_scaledboolean. - test:
use_all_data,fraction,npz_path(test suite, expects keynpz_key, defaultX),random_state.
Below are selected tables from the paper showcasing benchmark results.
Table I — Dataset Characteristics
| Dataset | # Features | # Instances | # Classes |
|---|---|---|---|
| Synth1 | 2 | 400 | 4 |
| Synth2 | 2 | 600 | 2 |
| IRIS | 4 | 150 | 3 |
| ADIMA | 19 | 1440 | 4 |
Table II — Results of Experiment 1
| Test Set Size | Neuron Coverage | Behavioral Coverage (BC) |
|---|---|---|
| 15 | 93% | 75% |
| 90 | 95% | 75% |
| 150 | 100% | 75% |
Table III — Model Summary for Conducted Experiments
| Experiment | Dataset / Model Type | Architecture |
|---|---|---|
| Experiment 1 | Synth1 / MLP | 1 hidden layer, 300 neurons |
| Experiment 2 | Synth2 / FFNN | 2 hidden layers: 60 & 20 |
| Experiment 3 | ADIMA / FFNN | 1 ReLU hidden layer |
| IRIS / FFNN | 2 hidden layers: 128 & 10 |
- Sample ONNX models and .npy data are included for quick testing.
- The properties/ directory contains formal property files used for verification experiments.
@inproceedings{akhiat2025covernet,
title={CoVerNet: Toward Coverage Testing for Neural Networks Based on Formally Verified Equivalence Classes},
author={Akhiat, Yassine and Daw, Zamira},
booktitle={2025 IEEE/AIAA 44th Digital Avionics Systems Conference (DASC)},
year={2025},
doi={10.1109/DASC66011.2025.11257196}
}
Apache License 2.0 — free for research and commercial use, with explicit patent grants for contributors and users.
This repository corresponds to the Beta implementation of the CoVerNet methodology. For any questions, feedback, or reports regarding the implementation or documentation, please contact:
-
Yassine Akhiat — yassine.akhiat@ils.uni-stuttgart.de
-
Zamira Daw — zamira.daw@ils.uni-stuttgart.de
Institute of Aircraft Systems (ILS) | University of Stuttgart | Germany