AAU logo

Department of Computer Science

Best Paper Award for model-checking paper

Professor Kim Guldstrand Larsen, Professor Jiri Srba and PhD student Søren Enevoldsen have been awarded the Best Paper Award at the European Joint Conferences on Theory and Practice of Software – ETAPS 2019.

Last modified: 21.05.2019

The European Association of Software Science and Technology, EASST, awarded the AAU researchers the prestigious award for their paper “Abstract Dependency Graphs and their Application to Model Checking” at the ETAPS 2019 conference in Prague in April.

Jiri Srba (left), Søren Enevoldsen (third from left) and Kim Guldstrand Larsen (right) at the award ceremony.

The paper, selected among more than 400 submissions, takes its point of departure in the researchers’ long-standing work within model-checking, including the development of the model checking tools UPPAAL and TAPAAL. 

For teaching purposes, a simplified version of a model checking tool, CAAL (Concurrency Workbench, Aalborg Edition), is used. Through extensive work on this, the researchers have refined the technologies behind the model checking tools and have shown how the use of dependency graphs can make it easier for the users of model checking tools to make a new inquiry in the tool. The new technology has already been implemented into both the UPPAAL and the TAPAAL tool. 

Screendump of the CAAL tool - see more at caal.cs.aau.dk 

“With this new technology implemented, we enable the users of the model checking tools to input information for a new inquiry much more simply and efficiently. If the user has input information into the different slots and made an inquiry, but wishes to make a new inquiry based on a different set of parameters, we now allow users to input new information – no matter what kind – into the slots, and the model-checker tool can analyze the system on the basis of this. In other words, this new technology has been shown to be the way to answer a wide range of questions much more simply and efficiently than the technology has allowed for until now,” Kim Guldstrand Larsen says.