This paper deals with systematic approaches for the analysis of stability properties and controller design for nonlinear dynamical systems. Numerical methods based on sum-of-squares decomposition or algebraic methods based on quantifier elimination are used. Starting from Lyapunov’s direct method, these methods can be used to derive conditions for the automatic verification of Lyapunov functions as well as for the structural determination of control laws. This contribution describes methods for the automatic verification of (control) Lyapunov functions as well as for the constructive determination of control laws.