SpaceEx is a new verification platform for hybrid systems that provides a scalable and efficient algorithm for reachability analysis. The algorithm uses polyhedra and support function representations to compute an over-approximation of reachable states. It improves upon previous methods by using variable time steps to ensure a given local error bound and introduces an improved approximation model that significantly enhances the algorithm's accuracy. The algorithm is implemented in SpaceEx, which includes a web-based graphical user interface and a model editor for creating complex hybrid systems. The paper presents a scalable reachability algorithm for hybrid systems with piecewise affine, non-deterministic dynamics. It combines polyhedra and support function representations to compute an over-approximation of reachable states. The algorithm uses variable time steps to guarantee a local error bound and an improved approximation model for better accuracy. The algorithm is implemented in SpaceEx, a new verification platform for hybrid systems, which includes a web-based graphical user interface and a model editor. The algorithm is tested on hybrid systems with more than 100 variables, demonstrating its scalability. The paper also discusses the use of support functions and template polyhedra for representing convex continuous sets, and presents a variable time-step algorithm for computing flowpipes. The algorithm is evaluated on various benchmarks, including a filtered oscillator and a helicopter controller, showing its effectiveness in handling complex dynamics and large state spaces. The results demonstrate the scalability and performance of the algorithm, as well as the effectiveness of the new approximation model in reducing error. The paper concludes that SpaceEx is a powerful tool for verifying hybrid systems with large state spaces and complex dynamics.SpaceEx is a new verification platform for hybrid systems that provides a scalable and efficient algorithm for reachability analysis. The algorithm uses polyhedra and support function representations to compute an over-approximation of reachable states. It improves upon previous methods by using variable time steps to ensure a given local error bound and introduces an improved approximation model that significantly enhances the algorithm's accuracy. The algorithm is implemented in SpaceEx, which includes a web-based graphical user interface and a model editor for creating complex hybrid systems. The paper presents a scalable reachability algorithm for hybrid systems with piecewise affine, non-deterministic dynamics. It combines polyhedra and support function representations to compute an over-approximation of reachable states. The algorithm uses variable time steps to guarantee a local error bound and an improved approximation model for better accuracy. The algorithm is implemented in SpaceEx, a new verification platform for hybrid systems, which includes a web-based graphical user interface and a model editor. The algorithm is tested on hybrid systems with more than 100 variables, demonstrating its scalability. The paper also discusses the use of support functions and template polyhedra for representing convex continuous sets, and presents a variable time-step algorithm for computing flowpipes. The algorithm is evaluated on various benchmarks, including a filtered oscillator and a helicopter controller, showing its effectiveness in handling complex dynamics and large state spaces. The results demonstrate the scalability and performance of the algorithm, as well as the effectiveness of the new approximation model in reducing error. The paper concludes that SpaceEx is a powerful tool for verifying hybrid systems with large state spaces and complex dynamics.