Formal Methods for Autonomous Vehicles

This article describes the impact that autonomous vehicle operation will have on a range of domains and how formal methods can guarantee the safe operation of those vehicles. The verification of the safe operation of autonomous systems (e.g., autopilot systems for commercial aircraft) was traditionally done using precise models and verification software based on formal methods. However, the increasing use of machine-learning-based subsystems (e.g., for perception) requires the use of different verification tools. We describe how formal methods are used today and how they will be adapted for future autonomous vehicles.