  The focus of this thesis is developing a framework for designing
correct-by-construction controllers using control certificates. We use
nonlinear dynamical systems to model the physical environment (plants). The
goal is to synthesize controllers for these plants while guaranteeing formal
correctness w.r.t. given specifications. We consider different fundamental
specifications including stability, safety, and reach-while-stay. Stability
specification states that the execution traces of the system remain close to an
equilibrium state and approach it asymptotically. Safety specification requires
the execution traces to stay in a safe region. Finally, for reach-while-stay
specification, safety is needed until a target set is reached.
  The design task consists of two phases. In the first phase, the control
design problem is reduced to the question of finding a control certificate.
More precisely, the goal of the first phase is to define a class of control
certificates with a specific structure. This definition should guarantee the
following: "Having a control certificate, one can systematically design a
controller and prove its correctness at the same time." The goal in the second
phase is to find such a control certificate. We define a potential control
certificate space (hypothesis space) using parameterized functions. Next, we
provide an inductive search framework to find proper parameters, which yield a
control certificate.
  Finally, we evaluate our framework. We show that discovering control
certificates is practically feasible and demonstrate the effectiveness of the
automatically designed controllers through simulations and real physical
systems experiments.

Systems and Control