Differential Dynamic Logic

We present the first approach for the combination of differential dynamic logic (dL) and NN verification. By joining forces, we can exploit the efficiency of NN verification tools while retaining the rigor of dL. This yields infinite-time horizon safety guarantees for neural network control systems.