Abstract:Providing formal guarantees for self-driving cars is a challenging task, since input-output space (i.e., all possible combinations of inputs and outputs) is too large to explore exhaustively. This paper presents an automated verification technique ensuring steering angle safety for self-driving cars by incorporating convex optimization and deep learning verification (DLV). DLV is an automated verification framework for safety of image classification neural networks. The DLV is extended by convex optimization technique in fail-safe trajectory planning to solve the judgement problem of predicted steering angle, and thus, to achieve verification of steering angle safety for self-driving cars. The benefits of the proposed approach are demonstrated on the NVIDIA's end-to-end self-driving architecture, which is a crucial ingredient in many modern self-driving cars. The experimental results indicate that the proposed technique can successfully find adversarial misclassifications (i.e., incorrect steering decisions) within given regions and family of manipulations if they exist. Therefore, the safety verification can be achieved (if no misclassification is found for all DNN layers, in which case the network can be said to be stable or reliable w.r.t. steering decisions) or falsification (in which case the adversarial examples can be used to fine-tune the network).