AAU logo
AAU tool remains among the best model checking tools in the world

AAU tool remains among the best model checking tools in the world

The TAPAAL team from the Department of Computer Science, Aalborg University took home four medals from the 2020 edition of the prestigious Model Checking Contest. The outcome emphasizes that the verification tool is among the best in the world.

Last modified: 25.06.2020

Over the years, a number of verification tools developed at the Department of Computer Science, Aalborg University have proved to be among the best model checking tools on the market. The outcome of the 2020 edition of the Model Checking Contest clearly supports this assumption. 

Earlier this week, the model checker tool TAPAAL, developed at AAU, won no less than two gold medals, one silver medal and one bronze medal in the prestigious contest, which was held online from Paris. Created in 2011, The Model Checking Contest is an annual event, where a team of researchers compares tools in various categories according to selected benchmarks to identify the best tools and techniques to handle given types of problems.

TAPAAL is a tool for modelling, simulation and verification of timed-arc Petri nets, and around 35 developers have contributed to the code over the past ten years. Today, the TAPAAL team is headed by Professor Jiri Srba together with Assistant Professor Peter G. Jensen, with massive student involvement and support. 

- We are happy that many years of hard work on TAPAAL has kept us in the elite of model checking developers, as demonstrated by our two gold, one silver and one bronze medal, Peter G. Jensen says.

He adds that the fact that TAPAAL won two less gold medals compared to last year, shows that the competition in the contest is as strong as ever:

- Going forward, we hope to stay in the lead next year - and maybe even (re)claim another gold medal. This will require research into new techniques and the discovery of new theory, something we are happy to have our skilled master students assist us with on a recurring basis.

Facts

The TAPAAL tool won the following medals:

  • CTL model checking: Gold
  • Global properties: Gold
  • Computation of upper bounds: Silver
  • Reachability: Bronze

For more information regarding TAPAAL, please visit the tool webpage​
To know more about the Model Checking Contest, please have a look here
 

For more information, contact:

Professor Jiri Srba
Department of Computer Science
Aalborg University
Phone:  2045 3514
E-mail: srba@cs.aau.dk

Assistant Professor Peter Gjøl Jensen
Department of Computer Science
Aalborg University
Phone: 6154 7278
E-mail: pgj@cs.aau.dk