Differential Game Logic

Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision
Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision

We extend the differential dynamic logic-based NN verification technique VerSAILLE (NeurIPS'24) to support verification under perturbations and leverage this result to derive end-to-end safety guarantees that carry over to fixed-point arithmetic implementations of (originally) real-valued NNs.

6. Oct 2025