People
Tomáš Dacík focuses on static analysis of programs. For his work he received the Brno Ph.D. Talent
Tomáš Dacík from FIT (Faculty of Information Technology) BUT (Brno University of Technology) focuses on static analysis of programs in his doctoral thesis. It verifies the properties of computer programs without having to run them and checks for errors. He has been working on this topic since his undergraduate study within the VeriFIT research group. And his research was so interesting that this year he received an award and a scholarship within the Brno Ph.D. Talent.
In his own words, Tomáš Dacík likes seemingly unsolvable problems and does not mind being, in the words of Jára Cimrman, a pioneer of dead ends. “In the context of my doctoral thesis as a whole, I don't suppose I ended up in a dead end. Similar research already exists. But of course, in the course of the process, one encounters partial mathematical or programming problems where one does not know in advance which direction to take. In that case, I just have to try a number of options and count on most of them being dead ends. Sometimes it's frustrating, but that's rare,” says Tomáš Dacík from FIT BUT.
He adds that his work is so much about experimentation and experimental measurement. “This is the great advantage of computer science. I can run the experimental verification right on my computer. I don't need expensive equipment, laboratories, chemicals,” he points out.
In his work, he focuses on static program analysis. “This means that I verify the properties of programs without the program having to run. Another program is written to study the one we are interested in. Program properties can also be verified dynamically. The program starts and monitors what it does. If there are no mistakes, if it is not running too slow,” Dacík explains in a simplified way. However, he says dynamic verification is not very efficient because only one run of the program is examined.
Tomáš Dacík focuses specifically on the analysis of programs that work with dynamically allocated memory. “This means that the program does not know in advance how much memory it will need. Memory is allocated on the run,” he says. This type of program may have bugs that only appear in certain operating systems, or that do not appear regularly but only randomly. “In this case, we then run the program once and it looks like everything is fine. But when it starts a second time, it might crash while running. That's why such mistakes are annoying. The second and absolutely crucial aspect is security. These errors are often the source of security vulnerabilities,” Dacík points out. Often these security vulnerabilities can be in browsers. “Everyone uses these and they are quite critical because we trust browsers with our passwords, for example. According to analyses by Microsoft and Google, up to 70 percent of errors originate from working with dynamically allocated memory,” adds Tomáš Dacík.
His work is still in the basic research phase and is looking at how to represent the configuration of these programs, using separation logic to do so. “From a programmer's perspective, this can be thought of as a data structure that allows infinite sets of memory configurations to be described in an efficient way. Simply put, I focus on designing operations over a data structure,” he says. In the second part, he would like to integrate the methods into the Broom program analyser, which is being developed by the VeriFIT research group at FIT BUT in cooperation with TU Wien, and possibly into another tool. “I am continuing my diploma thesis, which I would like to improve and refine the results so that they can be really used in a program analyser. In the long term, I would like to contribute to moving the topic from academia to industry,” he adds.
His research and current results so impressed the expert committee that this year Tomáš Dacík became one of the awarded doctoral students within the Brno Ph.D. Talent. “It was a very interesting experience for me. Final presentations are very short, so one has to fine tune every single slide and speak to the point and clearly. At the same time, the committee includes both academics and people from companies, so they have to convince them not only of the quality of their research, but also of its applicability in practice. I take the fact that I was finally awarded and received a scholarship as motivation and confirmation that I am doing my job well. At the same time, it is also a commitment to continue,” concludes Tomáš Dacík.
(zeh)
Matús Nosko from FIT BUT came up with an original ecosystem for smart homes. His equipment sells by the dozens
Doctoral students in engineering study the behaviour of the circulatory system. Neural networks also help them
FIT BUT scientists are developing an app for psychotherapists. Using deep learning, they aim to analyse therapy sessions
Sensorie greenhouse wants to make growing vegetables at home the norm. It offers smart solutions for year-round harvesting
FIT scientists want to prevent pilots from being blinded by lasers. They are developing a security system that will find the attacker