Automated Reasoning in the Real World: Towards Design Automation for Cyber-Physical Systems

Gao200_0.jpg
Sicun Gao

Speaker:  Sicun (Sean) Gao, Postdoctoral Researcher, MIT Computer Science and Artificial Intelligence Lab

Date: Friday, March 10, 2017
Time:  11am
Location:  Room 1202, CSE Building

Abstract:   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.

Bio:  Sicun Gao is a postdoctoral researcher at the MIT Computer Science and Artificial Intelligence Lab. He develops design automation techniques for cyber-physical and AI systems. His thesis work established the foundation for an algorithmic framework for the design and analysis of highly complex cyber-physical systems, for which he received his PhD in 2012 with honorable mention for the Carnegie Mellon School of Computer Science Distinguished Doctoral Dissertation award. He has subsequently devoted his postdoctoral research to the implementation and application of the framework as a practical tool named dReal. The tool has now been used in over 20 research groups across academia and industry, such as for designing autonomous cars at the Toyota Research Institute, and for personalized treatment for psoriasis that will soon enter clinical trials at a UK hospital. He is a co-PI of the NSF Large CPS Grant “Compositional, Approximate, and Quantitative Reasoning for Medical Cyber-Physical Systems.” His work received a silver medal for the Godel Research Prize Fellowship from the Kurt Godel Society.

Related Research Publications
http://scungao.github.io/papers/delta_complete_decision_procedures.pdf
http://scungao.github.io/papers/sat_mod_odes.pdf

Faculty host: CSE Prof. Rajesh Gupta