David Kozák and František Vídeňský from the Institute of Intelligent Systems will defend their doctoral thesis in December

We invite you to attend the defense of the doctoral thesis of Ing. David Kozák from the Department of Intelligent Systems, FIT BUT, which will take place on Wednesday, December 10, 2025, at 10:30 a.m. in meeting room G108 at FIT VUT. The supervisor of the dissertation entitled "New methods of static analysis not only for ahead-of-time compilers of object-oriented languages" is Prof. Tomáš Vojnar.

David Kozák's dissertation deals with the use of static analysis methods in the context of ahead-of-time compilation of object-oriented languages such as Java. Kozák focuses on the possibilities of applying these techniques in automated analysis and, at the same time, in the field of software architecture reconstruction in a microservices environment. David's research work has a specific application level. The tool in which he implemented most of his research is called GraalVM Native Image. It performs ahead-of-time compilation and has been under development for a long time at the Oracle Labs research institute. Kozák is part of the GraalVM team there.

The main goal of the author's work was to streamline the chain of processes connecting points-to static analysis and the subsequent work of the ahead-of-time compiler. Static analysis can be broadly defined as anything that analyzes a program without running it, with the aim of determining the properties of the program or verifying that it works correctly according to a specified definition of correctness. From the outset, this method has been closely linked to compilers. Static analysis applied to the compiler environment must be fast, efficient, and computationally inexpensive. The specific goal of the author's research was to maintain the reliability and accuracy of points-to static analysis, but at the same time to speed it up, i.e., to approximate the strength of another type of static analysis: rapid type. In addition, this had to be achieved in an ahead-of-time compiler environment, in this case working with a low-level representation of the Java programming language called bytecode. As the name suggests, ahead-of-time compilation into machine code takes place before the program is run as a separate process, only once and without the "luxury" of being able to subsequently interpret code that has not been compiled or, if necessary, recompile certain methods at runtime. Therefore, everything that could be executed is compiled, which is computationally demanding by its very nature, and the resulting binary file is usually large. This is where the motivation lies to streamline and speed up static analysis while maintaining its correctness.

The Native Image compiler that Kozák works with uses type points-to analysis working with object types (classes). Kozák used the saturation technique, which can be simplified as a compromise between points-to analysis and rapid-type analysis. Its main idea can be described as follows: We look at which specific implementations of a given type have been created (instantiated) and use only those. We cover the parts of the program that we can analyze accurately with points-to analysis methods. Conversely, if we have too much data available for some parts of the program, we use rapid-type analysis for them. The result is accuracy close to the outputs of points-to analysis and speed very close to that offered by rapid-type analysis.

Another part of Kozák's dissertation and research task was the design of an extension to the Native Image tool's points-to analysis called SkipFlow. This extension now tracks not only objects but also the flow of primitive values, while using predicate edges to prevent the propagation of values from unreachable branches (dead code) of the program. SkipFlow reduced the load on the compiler and offered more accurate analysis at the cost of a slight increase in runtime and with the benefit of subsequent faster work by the compiler itself.

Kozák's research also has a second, perhaps somewhat surprising and atypical field of application for static analysis – the sphere of microservices, or rather understanding the impact of their interdependencies. And this is more the domain of software engineering. Today, applications are developed in the form of a series of smaller microservices. The problem, however, is that it is difficult to track the communication between individual parts and the impact of changes in individual microservices on other services. Kozák again used the Native Image tool, this time to obtain information about each individual service, and then used this to create a holistic view of the entire application. The compiled version of the application can thus be used to reconstruct the high-level architecture and its completely up-to-date visualization, which can be passed on to the software architect. Kozák also participated in the creation of the SAVAT tool, which is capable of analyzing the impact of changes within the time series of individual microservice versions. Bottom line: David Kozák's dissertation is a step towards unifying three previously largely separate areas: compilers, interprocedural static analysis covering the entire program, and software engineering.

When asked about the key results of his research, David Kozák is clear: "I am most proud of SkipFlow, an extension of points-to analysis that tracks primitive values and monitors dependencies between program branches. Why? Because we have achieved the ideal result here: we have created an analysis that is both more accurate and faster. Then I would mention saturation, because by combining two types of analysis and calculating very accurately only where it makes sense, we were able to achieve almost identical results to a more accurate analysis, but in significantly less time." However, when taking stock, David also mentions more general points: "I am satisfied that this is not purely basic research, but that everything is integrated into a real tool, Native Image, and that saturation and SkipFlow are automatically enabled in this tool. This means that anyone who uses Native Image also uses the results of my dissertation. I like to focus my research on what is used in practice. I enjoy contact with industry and the real-world application of technology." David would like to thank his colleagues from the VeriFIT research group for their consultation and support during his research. As for his future work plans, he states that he would like to continue to straddle academic research and industry. His dream goal is to assemble a larger team of people who would participate in research within the GraalVM team, including bachelor's and master's students interested in compilers.

We would like to add that another public defense of a doctoral thesis is planned at our faculty in the same week. The author of the dissertation "Late Binding of Variables in AgentSpeak(L) Interpreters" is Ing. František Vídeňský from the Department of Intelligent Systems, and his supervisor is doc. František Zbořil. The public defense of this dissertation will take place on Friday, December 12, 2025, at 1:00 p.m. in room G108.

We wish both researchers continued success and joy in their field.