Formal methods are crucial for building computing systems that physically engage us in safety-critical ways such as airplanes, cardiac pacemakers, and nuclear plants. I will present a framework that aims to accomplish the following:
- Understand the computational complexity of controlling nonlinear and hybrid physical systems. Such problems are commonly considered to be highly undecidable because of the involvement of real numbers, differential equations, and so on. I show how reasonable upper bounds can be obtained through a practical formulation.
- Enhance automation in the design and implementation of control systems through automated reasoning engines. These engines are designed to cope with NP-hard problems, matching the complexity of the problems to be solved. The key is to engineer exponential algorithms to behave well in practice, by combining the full power of logical reasoning and numerical algorithms. I introduce our solver dReal and some promising experimental results.
- Certify correctness of control software through formal proofs. All algorithms that are used for the design and analysis of these systems should produce mathematical proofs that can be machine-checked. This requires a thorough logical analysis of techniques in control theory and numerical computing.