A Formally Verified Motion Planner for Autonomous Vehicles
ATVA, pp. 75-90, 2018.
Autonomous vehicles are safety-critical cyber-physical systems. To ensure their correctness, we use a proof assistant to prove safety properties deductively. This paper presents a formally verified motion planner based on manoeuvre automata in Isabelle/HOL. Two general properties which we ensure are numerical soundness (the absence of flo...More
Full Text (Upload PDF)
PPT (Upload PPT)