Este documento trata sobre enfoques sistemáticos para el análisis de propiedades de estabilidad y diseño de controladores para sistemas dinámicos no lineales. Se utilizan métodos numéricos basados en la descomposición de sumas de cuadrados o métodos algebraicos basados en la eliminación de cuantificadores. Partiendo del método directo de Lyapunov, estos métodos pueden utilizarse para derivar condiciones para la verificación automática de funciones de Lyapunov, así como para la determinación estructural de leyes de control. Esta contribución describe métodos para la verificación automática de funciones de Lyapunov (de control), así como para la determinación constructiva de leyes de control.