{"id":"arxiv/2606.16567","url":"https://arxiv.org/abs/2606.16567","tags":["cs.AI","cs.LG","eess.SY","math.DS"],"score":0,"title":"TNODEV: Toolbox for Neural ODE Verification","domain":"cs.AI","source":"arxiv","authors":["Abdelrahman Sayed Sayed","Pierre-Jean Meyer","Mohamed Ghazel"],"reviews":0,"subject":"cs.AI","summary":"Neural ordinary differential equations (neural ODE) gained attention in safety critical settings such as continuous-time controllers for cyber-physical systems and classifiers integrated into automated decision pipelines, raising the question whether their behavior can be formally verified. Existing tools dedicated to neural ODE provide only a single reachability call without iterative input-set refinement, limiting the precision of their verdicts to whatever one reachability call can deliver. We present TNODEV, the first formal verifier for neural ODE that integrates a falsification…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-06-15","reactions":{}}