We face grand new challenges as computer systems start engaging us physically with high levels of autonomy. For example, it is extremely difficult to build autonomous cars with safety guarantees, for two main reasons. First, their tight integration of computational and mechanical components generates behaviors that are not well-studied in either computer science or control engineering. Second, they are driven by modern AI algorithms that complicate software execution flows with monstrous nonlinear functions and error-prone numerical computation. Interestingly, both aspects of difficulty come from a common source: the hybridization of elements from two distinct domains. One is digital, logical, and discrete, while the other is analog, numerical, and continuous. My research addresses this fundamental difficulty in the cyber-physical domain, using an algorithmic approach that breaks down the barriers between the discrete and the continuous.
I will present the theories, algorithms, and practical tools developed in an automated reasoning framework that tackles the core computational challenges in cyber-physical systems design, by combining the full power of combinatorial search, numerical optimization, and statistical learning. The proposed methods provide formal reliability guarantees that can not be obtained through simulation and testing. I will show examples of successful applications in safe autonomous driving, personalized medicine, and security of critical infrastructures. I will also discuss how the work on design automation for cyber-physical systems can lead to the convergence of the first wave (symbolic reasoning) and second wave (statistical learning) of AI, towards a powerful algorithmic engine that is crucial for solving challenging problems in a broad range of engineering domains.