A hybrid automaton is a mathematical model in which real-valued variables are subject to time-driven as well as event-driven changes. The time-driven change is modeled with differential equations (or inclusions), and different sets of such equations can be associated with different locations (modes) of the automaton. The event-driven changes are associated with the transitions of the automaton, and are modeled by reset maps that reflect an instantaneous change of the variables. Hybrid automata are difficult to analyze, because even a small variation in states or parameters, or small error in the analysis algorithm could possibly lead to qualitatively different behaviors. We compute the set of reachable states of the automaton. Using set-based computations allows us to incorporate comutation errors such that the resulting set is a conservative overapproximation of the actual solution. The difficulty is to find set representations for which the necessary operators are efficient to compute, and yet provide satisfactory precision. In SpaceEx, our tool platform for verifying hybrid automata, we have implemented an algorithm that uses two set representations, polyhedra and support functions, to obtain maximum scalability. At each step of the algorithm, we choose the representation that provides the best compromise between speed and accuracy, based on the data and operator. In this talk, we present SpaceEx and discuss how combining different set representations help us gain efficiency.