# Verifying Aircraft Collision Avoidance Neural Networks Through Linear Approximations of Safe Regions

arXiv: https://arxiv.org/abs/1903.00762 · HTML: https://mlsanity.com/paper/1903.00762/

## Key facts

- Cited by 9 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 2 Mar 2019.

## Built on by (most cited first, 9 of 9)

- [How to Certify Machine Learning Based Safety-critical Systems? A Systematic Literature Review](https://mlsanity.com/paper/2107.12045/) (2021)
- [Towards Practical Robustness Analysis for DNNs based on PAC-Model Learning](https://mlsanity.com/paper/2101.10102/) (2021)
- [Provably Safe Neural Network Controllers via Differential Dynamic Logic](https://mlsanity.com/paper/2402.10998/) (2024)
- [Generating Probabilistic Safety Guarantees for Neural Network Controllers](https://mlsanity.com/paper/2103.01203/) (2021)
- [A Robust Optimisation Perspective on Counterexample-Guided Repair of Neural Networks](https://mlsanity.com/paper/2301.11342/) (2023)
- [VeriCompress: A Tool to Streamline the Synthesis of Verified Robust Compressed Neural Networks from Scratch](https://mlsanity.com/paper/2211.09945/) (2022)
- [Patch Synthesis for Property Repair of Deep Neural Networks](https://mlsanity.com/paper/2404.01642/) (2024)
- [Aircraft Collision Avoidance Systems: Technological Challenges and Solutions on the Path to Regulatory Acceptance](https://mlsanity.com/paper/2510.20916/) (2025)
- [Provable Repair of Deep Neural Network Defects by Preimage Synthesis and Property Refinement](https://mlsanity.com/paper/2511.07741/) (2025)

## Abstract (arXiv)

The next generation of aircraft collision avoidance systems frame the problem as a Markov decision process and use dynamic programming to optimize the alerting logic. The resulting system uses a large lookup table to determine advisories given to pilots, but these tables can grow very large. To enable the system to operate on limited hardware, prior work investigated compressing the table using a deep neural network. However, ensuring that the neural network reliably issues safe advisories is important for certification. This work defines linearized regions where each advisory can be safely provided, allowing Reluplex, a neural network verification tool, to check if unsafe advisories are ever issued. A notional collision avoidance policy is generated and used to train a neural network representation. The neural networks are checked for unsafe advisories, resulting in the discovery of thousands of unsafe counterexamples.