In this paper we present the continuous and on-going development of datastructures and algorithms underlying the verification engine of the tool UPPAAL. In particular, we review the datastructures of Difference Bounded Matrices, Minimal Constraint Representation and Clock Difference Diagrams used in symbolic state-space representation and -analysis for real-time systems. In addition we report on distributed versions of the tool, and outline the design and experimental results for new internal datastructures to be used in the next generation of UPPAAL. Finally, we mention work on complementing methods involving acceleration, abstraction and compositionality.