ACAS-Xu-Verification-using-Z3

This repository provides a framework for verifying properties of ACAS Xu neural networks.

Verification is performed using the Z3 SMT solver.

I changed some lines of code ('Be careful').

Data Files

You'll need to download the necessary ONNX and vnnlib files. For this example

• ONNX: ACASXU_run2a_2_2_batch_2000.onnx
• Property: prop_1.vnnlib
• If you need a textual description of the properties, see here: https://github.com/mldiego/AcasXu/blob/master/Properties/