Skip to main content.
Figure 1: Uppaal on screen.

Uppaal is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays, etc.).

The tool is developed in collaboration between the Department of Information Technology at Uppsala University, Sweden and the Department of Computer Science at Aalborg University in Denmark.


News: The current official release is Uppaal 4.0.15 (November 18, 2019).

Since Feb 26 2008, we also distribute development snapshots of the tool. The current version is 4.1.24 released November 26th, 2019.

Uppsala Universitet Aalborg University


The Uppaal tool is free for non-commercial applications in academia only. For commercial applications a commercial license is required. Please see the Download section or for more information.

To find out more about Uppaal, read this short introduction. Further information may be found at this web site in the pages About, Documentation, Download, and Examples.

Mailing Lists

Uppaal has an open discussion forum group at Google Groups intended for users of the tool. To join or post to the forum, please refer to the information at the discussion forum page. There is also Uppaal tag on Stackoverflow. Bugs should be reported using the bug tracking system. To email the development team directly, please use uppaal(at)list(dot)it(dot)uu(dot)se.


In our ongoing work to localize the Uppaal GUI we would like to acknowledge contributions by the following external people:

  • Dmitry Ivanov (RU)
  • Hiroshi Fujimoto (JA)
  • Line Juhl (DK)
  • Shuhao Li (ZH)
  • Marius Mikucionis (LT)