The paper presents a scalable reachability algorithm for hybrid systems with piecewise affine, non-deterministic dynamics. The algorithm combines polyhedra and support function representations of continuous sets to compute an over-approximation of reachable states. It improves upon previous work by using variable time steps to guarantee a given local error bound and proposes an improved approximation model that significantly enhances the accuracy of the algorithm. 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. Experimental results demonstrate the scalability and performance of the tool, handling hybrid systems with more than 100 variables. The paper also discusses the efficiency of the algorithm in computing transition successors and the use of clustering to avoid an exponential blowup in the number of sets.The paper presents a scalable reachability algorithm for hybrid systems with piecewise affine, non-deterministic dynamics. The algorithm combines polyhedra and support function representations of continuous sets to compute an over-approximation of reachable states. It improves upon previous work by using variable time steps to guarantee a given local error bound and proposes an improved approximation model that significantly enhances the accuracy of the algorithm. 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. Experimental results demonstrate the scalability and performance of the tool, handling hybrid systems with more than 100 variables. The paper also discusses the efficiency of the algorithm in computing transition successors and the use of clustering to avoid an exponential blowup in the number of sets.