Automated Reasoning for Nonlinear Control

Automated reasoning develops combinatorial search and optimization algorithms that are crucial for the reliable engineering of digital systems, from hardware to software. Despite the clear NP-hardness of these problems, significant progress has been made in the past decades for solving large instances of practical relevance.  There is a seemingly-wide gap between the discrete/combinatorial setting of automated reasoning and the continuous/analytic one for dynamics and control. I will show that this divide is artificial and eliminable, and doing so is crucial for the next steps in nonlinear control. As an example I will describe neural certificate methods that exploit recent advances in learning and reasoning, for synthesizing nonlinear control systems that are hard to manually analyze but can nonetheless aim to provide rigorous guarantees of stability and safety.