Swarm robotics is an active research area where large groups of simple robots are developedto perform complex tasks. It has various potential applications such as surveillance, warehouse logistics, and collective construction, because of its large sensing capability, fault tolerance, and collaboration skills that are impossible to a single robot. However, controlling swarm robots to perform high-level tasks automatically and verifiably remains challenging due to the large state space. In this work, I present the verifiable control framework for swarm robots from high-level specifications in different combinations of 4 dimensions: symbolic/continuous levels, centralized/decentralized methods, navigation/formation-based specifications, and non-reactive/reactive tasks. The first contribution of the work is a top-down control framework for non-reactive navigation swarm tasks. At the symbolic level, I propose an integer programming-based method for executing a centralized symbolic plan, and compare it with existing decentralized execution in terms of task efficiency, failure resilience, and computational complexity. At the continuous level, I propose a control barrier function based method which guarantees correct (satisfy all specifications) and safe (no collision) transitions when robots execute the high-level tasks. The trade-offs between centralized and decentralized methods provide guidance to swarm controls to achieve different purposes under different restrictions. The second contribution is a novel abstraction and grammar for location and formation-based swarm specifications. With the proposed abstractions, we developed a centralized control synthesis approach which guarantees that the specified swarm behaviors will be satisfied if feasible. This contribution expands the task space of swarms, and gives insights into controlling a large fleet of autonomous robots to perform complex tasks which require composition of behaviors and coordination of different sub-swarms. The third contribution is an extension to the second, which automatically synthesizes controls for swarms to achieve reactive formation tasks in a decentralized manner. This work utilizes an integer programming-based method to calculate constraints on subswarm sizes given the reactive finite state machine, to ensure a priori feasibility of the task. In addition, a decentralized auction-based algorithm is developed for executing the reactive finite state machine, which satisfies the robot number constraints. Such decentralized frameworks increase the scalability of control synthesis and can be applied to swarm systems with a larger number of robots. The last contribution of this thesis is an automatic approach to redistributing robots according to user requests during the task execution while maintaining the original specifications. The approach includes creating symbolic plans, limiting robot numbers given the constraints, and ensuring all robots to satisfy safety requirements of the given highlevel tasks. This work further enhance the flexibility and reactivity of swarms performing high-level tasks.