Formal verification of octorotor flight envelope using barrier functions and SMT solving