Not all automatons are the same. A student of FIT uses büchi automata to improve program analysis

The name of Barbora Šmahlíková, a student of the FIT (Faculty of Information Technology) BUT (Brno University of Technology), has been resonating in her field for the last six months. She has succeeded in improving the algorithm for Büchi automata. This has significantly improved the efficiency of calculating their complementation, which can be used, for example, for termination analysis of programs.

Today, her improved algorithm is even considered one of the world's best. For her work, she was named the recipient of The Award of the Czech Government for a Gifted Student on 27 January 2023 by the Research, Development and Innovation Committee (RDIC). She received the award on Thursday 8 June at the Hrzánský Palace in Prague. She also won the Rector's Award at the Academic Assembly in 2022, received the Zdena Rábová Award and made it to the final line-up of 8 competitors in the BUT University Competition.

She started her research almost at the beginning of her bachelor studies and came to the topic of her bachelor thesis almost like a blind man to a violin, because it was assigned to her. “I definitely didn't have a clear idea of what I wanted to do. All I knew was that I wanted to try to work in research while doing something related to mathematics. Then I heard about the opportunity to get involved, but I didn't have the courage. I couldn't imagine coming up with anything on my own. But then they approached me directly, so I finally got involved and found myself in the topic – even though it took me over half a year to understand the algorithm enough to improve it,” Barbora says. She decided to continue the topic and devoted herself to it in her bachelor thesis.

Her work in the area of algorithm development for so-called omega automata soon resulted in publications at international conference forums, mostly reserved for doctoral students. And what exactly is the magic of Büchi's automata? It is an abstract model that can be used to model a system and then observe some of its properties. “I have one master automaton for a system, say a Model A, and I want to test a feature of it. So I create an automaton B for this property and using complementation I can check whether this property is valid for the system or not,” Barbora explains. “This way we can verify, for example, that a program, such as an operating system, computer game, etc., will never crash,” he adds.

However, there can be such a huge number of ways in which the system can behave that there is a risk that the computer could run out of memory before it is possible to determine whether the program satisfies the property we have tested. Therefore, it is necessary to make the algorithm as efficient as possible and not use so much memory.This can be achieved by some optimizations, which Barbora is working on.

Barbora is still working on the algorithm, and she is also researching other automata – she is now working on ELA automata, which work on a similar principle. What would be complicated to represent using Büchi automata is easier to represent using ELA automata. She is therefore exploring another method that could be even more effective in the future.