Optimization Based Verification and Synthesis for Safe Autonomy

Autonomous systems should satisfy a set of requirements that guarantee their safety, efficiency, and reliability when working under uncertain circumstances. These requirements can have financial, or legal implications or they can describe what is assigned to autonomous systems.As a result, the system controller needs to be designed in order to comply with these - potentially complicated - requirements, and the closed-loop system needs to be tested and verified against these requirements. However, when the complexity of the system and its requirements increases, designing a requirement-based controller for the system and analyzing the closed-loop system against the requirement becomes very challenging. In this case, existing design and test methodologies based on trial-and-error would fail, and hence disciplined scientific approaches should be considered. To address some of these challenges, in this dissertation, I present different methods that facilitate efficient testing, and control design based on requirements: 1. Gradient-based methods for improved optimization-based testing, 2. Requirement-based learning for the design of neural-network controllers, 3. Methods based on barrier functions for designing control inputs that ensure the satisfaction of safety constraints.