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.
The TAPAAL tool won the following medals:
- CTL model checking: Gold
- Global properties: Gold
- Computation of upper bounds: Silver
- Reachability: Bronze