UPPAAL is a tool suite designed for the automatic verification of safety and bounded liveness properties in real-time systems modeled as networks of timed automata. Developed through a collaboration between BRICS at Aalborg University and the Department of Computing Systems at Uppsala University, UPPAAL includes a graphical interface for representing networks of timed automata, a compiler for transforming linear hybrid systems into timed automata, and a model-checker based on constraint-solving techniques. The tool also supports diagnostic model-checking, providing information when verification fails. Key features include on-the-fly verification, symbolic techniques to handle state explosion, and syntactic checks. UPPAAL is implemented in C++ and is available via its official website. This paper provides an overview of UPPAAL's features, theoretical foundations, and applications.UPPAAL is a tool suite designed for the automatic verification of safety and bounded liveness properties in real-time systems modeled as networks of timed automata. Developed through a collaboration between BRICS at Aalborg University and the Department of Computing Systems at Uppsala University, UPPAAL includes a graphical interface for representing networks of timed automata, a compiler for transforming linear hybrid systems into timed automata, and a model-checker based on constraint-solving techniques. The tool also supports diagnostic model-checking, providing information when verification fails. Key features include on-the-fly verification, symbolic techniques to handle state explosion, and syntactic checks. UPPAAL is implemented in C++ and is available via its official website. This paper provides an overview of UPPAAL's features, theoretical foundations, and applications.