# Self-Driving Vehicle Verification Towards a Benchmark

arXiv: https://arxiv.org/abs/1806.08810 · HTML: https://mlsanity.com/paper/1806.08810/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 20 Jun 2018.

## Built on by (most cited first, 1 of 1)

- [Monitoring of Perception Systems: Deterministic, Probabilistic, and Learning-based Fault Detection and Identification](https://mlsanity.com/paper/2205.10906/) (2022)

## Abstract (arXiv)

Industrial cyber-physical systems are hybrid systems with strict safety requirements. Despite not having a formal semantics, most of these systems are modeled using Stateflow/Simulink for mainly two reasons: (1) it is easier to model, test, and simulate using these tools, and (2) dynamics of these systems are not supported by most other tools. Furthermore, with the ever growing complexity of cyber-physical systems, grows the gap between what can be modeled using an automatic formal verification tool and models of industrial cyber-physical systems. In this paper, we present a simple formal model for self-deriving cars. While after some simplification, safety of this system has already been proven manually, to the best of our knowledge, no automatic formal verification tool supports its dynamics. We hope this serves as a challenge problem for formal verification tools targeting industrial applications.