Verificación formal de la envolvente de vuelo del octorotor mediante funciones de barrera y resolución SMT