Verification of Autonomous Neural Car Control with KeYmaera X

Enguerrand Prebet, Samuel Teuber, André Platzer

This article presents a formal model and formal safety proofs for the ABZ'25 case study in differential dynamic logic (dL). The case study considers an autonomous car driving on a…