A Formally Verified Motion Planner for Autonomous Vehicles

ATVA, pp. 75-90, 2018.

Cited by: 9|Bibtex|Views6
EI
Other Links: dblp.uni-trier.de|academic.microsoft.com

Abstract:

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

Code:

Data:

Your rating :
0

 

Tags
Comments