Fully automated driving of cars on a motorway has gained much visibility to the general public over the last years. However, to be usable the safety of the system, consisting of hardware and software, needs to be certified. Formal verification has been identified as a usable approach to ensure such safety requirements.

To prove safety of a self-driving car we first have to model the car and the environment of the car in a formal system. Then we prove in this formal system that all unsafe states are not reachable. This is difficult, because the continuous dynamics and the discrete logic make the car a hybrid system, which are difficult to analyse. Furthermore, the other cars also are hybrid systems, which makes the complete model a system of systems.

Multi-Lane Spatial Logic (MLSL) is a dedicated formal system to reason about spatial properties, such as collision freedom, of traffic manoeuvres on a motorway from the local perspective of a car. We can model the controller of a car in MLSL. While there already exist proofs of safety for controllers of traffic manoeuvres modelled in MLSL, these proofs were found manually and in these proofs all data is assumed to be correct. This is an unrealistic assumption.

In this thesis we develop methods to automatically prove safety of the controller of a self-driving car. In our proofs we pay special attention to the fact that often the controller has to work with imperfect data.

We automate proving safety of controllers of self-driving cars, while allowing for two different kinds of errors. The first kind of error is that some cars may not be visible to the car under consideration, e.g. because they are hidden by another car. The second kind of error is that spatial information, such as distances, may be known only approximately, e.g. because the sensors are not perfect. We extend MLSL to be able to reason about safety despite these kinds of errors. Additionally, we
study meta-logical properties of MLSL with our extension, such as whether satisfiability is decidable.