Design of guaranteed safe maneuvers using reachable sets: Autonomous quadrotor aerobatics in theory and practice