Assured Autonomy Tools Portal
Continual Assurance of Learning-Enabled, Cyber-Physical Systems (LE-CPS)

Formal Analysis of Neural Network-based Systems in the Aircraft Domain


Neural networks are being increasingly used for efficient decision making in the aircraft domain. Given the safety-critical nature of the applications  involved, stringent safety requirements must be met by these networks. In this work we present a formal study of two neural network-based systems developed by Boeing. The Venus verifier is used to analyse the conditions under which these systems can operate safely, or generate counterexamples that show when safety cannot be guaranteed. Our results confirm the applicability of formal verification to the settings considered.

Year of Publication
Conference Name
The 24th International Symposium on Formal Methods (FM21)