CAV Award 2013

The CAV Award for 2013 has been presented to Kim G. Larsen, Paul Pettersson and Wang Yi for their seminal work on Uppaal, which is the foremost tool suite for the verification of real-time systems and the synthesis of real-time controllers. Congratulations to the awardees for receiving this well deserved accolade and to the award committee for making such an excellent choice!

If you are interested in using the tool for research and/or teaching, simply download it and read this tutorial by Frits Vaandrager. You will be up and running in no time. 


Uppaal has its roots in a tool originally developed in Uppsala and described in the conference paper Automatic verification of real-time communicating systems by constraint-solving co-authored by Wang Yi, Paul Pettersson and Mads Daniels (Proceedings of FORTE 1994). Since then, Uppaal has been jointly developed by Kim G. Larsen's research group at Aalborg University and by the group led by Wang Yi at Uppsala University. In this period, Uppaal has become an industrial-strength tool for computer-aided verification of computing systems that has been applied to many case studies by several research groups in academia and industry. The efficiency of its computational engine has been improved greatly by theoretical and practical advances relying on highly non-trivial insights. Moreover, the tool now supports the analysis of quantitative extensions of timed automata, automatic model-based testing of real-time systems and the synthesis of controllers in the context of timed games. It is still under continuous development.

Overall, the Uppaal tool is a real success story for the research community working on automated verification of computer systems. As all long-term research and tool development efforts, the work on Uppaal and its applications is due to many gifted researchers and their students. The CAV Award 2013 cannot recognize them all, but the list of authors of the many papers stemming from the work on UPPAAL gives a hint of the magnitude of the research effort involved in building such a tool over a period of nearly 20 years.