Formal Verificationfor Trillion Mile Challenge

Autonomous cars face two major challenges. First, the system needs to analyze large amounts of data from its dynamic environment, and react intelligently and quickly. Second, any such reaction needs to be safe; even a small probability of accident per mile can be catastrophic in a mass deployment. To achieve these two goals, our project aims to develop a unified framework that brings together the advances in machine learning and control that can make autonomous driving possible with the advances in verification that can make it safe. Our goal is to be able to rigorously characterize the safety envelopes of a real-world autonomous driving solution by combining data driven modeling of complex urban environments with new capabilities for analyzing complex control systems.