To design controllers for dynamical systems is to solve a special class of program synthesis problems. We exploit the connection between control theory and formal methods to develop automated methods for hybrid and nonlinear control.