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.