  This paper proposes a framework for automatic formal controller synthesis for
general hybrid systems with a subset of safety and reachability specifications.
The framework uses genetic programming to automatically co-synthesize
controllers and candidate Lyapunov-like functions. These candidate
Lyapunov-like functions are used to formally verify the control specification,
and their correctness is proven using a Satisfiability Modulo Theories solver.
The advantages of this approach are: no restriction is made to polynomial
systems, the synthesized controllers are expressed as compact expressions, and
no explicit solution structure has to be specified beforehand. We demonstrate
the effectiveness of the proposed framework in several case studies, including
nonpolynomial systems, sampled-data systems, systems with bounded
uncertainties, switched systems, and systems with jumps. osed framework in
several case studies, including nonpolynomial systems, sampled-data systems,
systems with bounded uncertainties, switched systems, and systems with jumps.
