Anna Bolotina receives teampool award for her master's thesis

October 16, 2025

Anna Bolotina received her bachelor’s degree from Southern Federal University in Russia in 2018 and her master’s degree from the University of Salzburg in 2024. She is currently a doctoral student in formal methods at the University of Salzburg under the supervision of Prof. Christoph Kirsch. From 2019 to 2022, she was a research assistant at the Czech Technical University in Prague and from 2022 to 2024 at the University of Salzburg. Her research focuses on programming languages and functional programming. She has now received the prestigious teampool award for her master’s thesis.

Her thesis, “Symbolic Benchmarking of RISC-V Code,” deals with symbolic benchmarking. What exactly does that mean, and why is it relevant?

Imagine a program that is supposed to analyze data. According to theory, it should be able to do this in 10 steps. Symbolic benchmarking can show whether the program is actually that efficient – or whether a small error suddenly means it needs 100 steps. Symbolic benchmarking is a new concept that can be used to find out how efficiently a computer program works – without actually running it. Instead of testing the program with lots of inputs, a technique called “symbolic execution” is used. The numerical values of variables are replaced by mathematical formulas. The number of calculation steps required is examined, depending on how large or complex the input is. The method helps to identify whether a program is working correctly or contains an error.

When did you first become interested in symbolic benchmarking?

I met Professor Christoph Kirsch, my main supervisor, when I was working as a research assistant in Prague. He suggested that I complete a master’s degree at the University of Salzburg, with the possibility of continuing as his doctoral student afterwards. At the time, he was working with one of his doctoral students on a toolchain for symbolic execution called Unicorn (note: a toolchain is a collection of software tools that work together to perform a specific task. In computer science, this often means different programs that are used sequentially or together to analyze, test, or improve a program, for example). I wanted to do a PhD and accepted his offer – so we started working on this topic together. The idea of symbolic benchmarking emerged during our collaboration.

Can you describe in layman’s terms what “symbolic execution” means and why it is so important?

Symbolic execution helps to automatically find errors in a program without actually running it with different input values. For example: A program calculates (a + b) / c and accepts the numerical values of the variables a, b, and c as input. It can fail if the value of c is equal to 0. Real programs process millions of values. Programmers usually check the correctness of a program through testing. But with thousands of conditions, it’s easy to overlook some cases. That’s why symbolic execution is important.

What practical applications could benefit from your research results?

More work is needed to make my results truly scalable. But in my opinion, they are potentially useful for complex, computationally intensive applications, as well as for interactive applications where high response speed is critical. Examples could include the modeling of physical processes such as climate models. Such processes often take a long time, and it is helpful to ensure that no computing time is wasted due to errors.

What challenges did you find particularly challenging in your research, and how did you overcome them?

The biggest challenge for me was my lack of background in computing systems, such as the Unicorn toolchain, which I started working with. What helped me were numerous discussions with my supervisors and the doctoral student who was also working on this topic with Professor Kirsch.

Is there a particular goal you would like to achieve in computer science?

That’s a difficult question. At the moment, I would say that I would like to make as many useful contributions to computer science as possible. I am also interested in various areas within computer science and enjoy learning new things, so my future research may also develop beyond the topic of symbolic execution.

What is it like to study at the University of Salzburg?

To be honest, the language barrier was a bit challenging for me, as most students spoke German among themselves and I only spoke English. But I also had a slightly different experience, as I was employed by the university for a project led by Professor Sebastian Forster, my second supervisor. I would like to take this opportunity to thank him for this wonderful opportunity. As a member of the department, I spent more time with other staff, doctoral students, and professors. The atmosphere among them was very friendly, and I also learned a lot.

About teampool

teampool personal service gmbh is one of Austria’s leading personnel service providers, specializing in temporary employment, personnel consulting, and engineering. At twelve locations, the team players take care of the needs of their customers, temporary workers, technicians, and applicants. The company stands for enthusiasm and is actively committed to promoting young talent in the field of computer science to meet the demand for skilled workers and drive innovative developments. By awarding scholarships to students at Paris Lodron University Salzburg, teampool not only aims to promote careers, but also to contribute to strengthening Austria as a location for innovation.

Next week, teampool personal service gmbh will award scholarships and bonuses to four computer science students at the University of Salzburg. This series showcases our award winners.

Tamara Stangl, BA MA MA

Universität Salzburg | Kommunikation und Fundraising

Kapitelgasse 6 | 5020 Salzburg | Austria

Tel: +43 662 8044-2026

E-Mail an Tamara Stangl, BA MA MA