### Abstract

The Vienna Convention on Road Traffic defines the safe distance traffic rules informally. This could make autonomous vehicle liable for safe-distance-related accidents because there is no clear definition of how large a safe distance is. We provide a formally proven prescriptive definition of a safe distance, and checkers which can decide whether an autonomous vehicle is obeying the safe distance rule. Not only does our work apply to the domain of law, but it also serves as a specification for autonomous vehicle manufacturers and for online verification of path planners.

### License

BSD License

### Topics

- Computer science/Algorithms/Mathematical
- Mathematics/Physics

### Session Safe_Distance

- Safe_Distance
- Safe_Distance_Reaction
- Evaluation

### Depends on

- Sturm’s Theorem

## Cite

×

Safe_Distance-AFP

    @article{Safe_Distance-AFP,
      author  = {Albert Rizaldi and Fabian Immler},
      title   = {A Formally Verified Checker of the Safe Distance Traffic Rules for Autonomous Vehicles},
      journal = {Archive of Formal Proofs},
      month   = {June},
      year    = {2020},
      note    = {\url{https://isa-afp.org/entries/Safe_Distance.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Jun 3, 2020 : Isabelle2020