Automated generation of dynamics-based runtime certificates for high-level control