teaching

2025

1. BSc

   Weak Dependencies for Side-Effecting Constraint Systems 🇪🇪

   Heigo Tornik

   University of Tartu, 2025

   Supervisors: Simmo Saan, Vesal Vojdani

   Abs HTML Code

   The bachelor’s thesis examines the static analysis method abstract interpretation, specifically side-effecting constraint systems. Constraint systems can be used to describe programs in an abstract manner and, by solving them with top-down solvers, such as TDside, several properties, like occuring errors, can be described. The thesis provides a theoretical background on constraint systems and the top-down solver TDside, and describes the inefficiency in TDside, where the program point that creates a thread depends on the thread being created, causing unnecessary recalculations. To solve the inefficiency, so-called “weak dependencies” are described. The right-hand side of the constraint system is supplemented by adding a new function demand and the necessary additions to TDside to solve these new constraint systems are described. In the thesis TDweak was created based on TDside in two variations: eager and lazy. Weak dependencies, when implemented in Goblint, reduced the number of right-hand side evaluations of constraint system by an average of 28.87% for the lazy variation and 13.70% for the eager variation.

2. BSc

   Improving Bitwise Operation Analysis in Goblint 🇪🇪

   Henrik Innos

   University of Tartu, 2025

   Supervisor: Simmo Saan

   Abs HTML Code

   Goblint is a static analyzer, based on abstract interpretation, specializing in multi-threaded C programs. The goal of this thesis is to improve the precision of Goblint’s static analysis by enhancing its handling of bit operations. The thesis establishes a set of integer properties that characterize their behaviour when subjected to bitwise operations on their machine representations, which were used to enhance the abstractions of logical bitwise operations in Goblint’s integer domains. Additionally, support for the analysis of bit-fields was added. The precision of Goblint’s analyses was successfully improved: the implementation was evaluated on SV-COMP benchmarks, resulting in Goblint being able to solve 26 additional tasks, and its correctness was formally proved.

3. BSc

   Migrating the “Automata, Languages and Compilers” Codebase to Java 21 🇪🇪

   Adeline Talvik

   University of Tartu, 2025

   Supervisor: Simmo Saan

   Abs HTML

   Over the years, the Java programming language has been updated with many code constructs which make programming easier and reduce boilerplate code, such as record patterns and pattern matching for switches. The goal of this Bachelor’s thesis was to modernise the codebase for the Java-based course “Automata, Languages and Compilers”. This included replacing the Visitor design pattern with alternatives, converting classes to records, converting abstract classes to sealed interfaces and updating methods. By the end of the modernisation process, the line count of the code repository was reduced by approximately 4000, despite the added files and documentation.

2024

1. BSc

   Widening Operators in the Abstract Interpretator Goblint 🇪🇪

   Ronald Judin

   University of Tartu, 2024

   Supervisor: Simmo Saan

   Abs HTML Code

   Static analysis of programs is used to ensure the correctness and safety of software. Abstract interpretation is a method of static analysis used by the abstract interpretator Goblint. Widening is a method in abstract interpretation to ensure the convergence of analysis of cycles. There are many widening operators defined in Goblint. This paper describes them and the implementation of new ones. The newly implemented widening operators were successfully tested.

2. BSc

   GobExec: Benchmarking Framework for Program Analysis Tools 🇪🇪

   Evaldas Petnjunas

   University of Tartu, 2024

   Supervisor: Simmo Saan

   Abs HTML Code

   Goblint is a static program analysis tool which uses a benchmarking suite for ensuring soundness and effectiveness of its analyses. The current solution for benchmarking relies on a set of Ruby scripts which have become unmaintainable and difficult to extend. This thesis describes a unified benchmarking framework for program analysis tools in Python programming language. The framework provides at least the same functionality as the old solution for benchmarking, while making the porting and replacing of old benchmarking scripts to Python possible. The new framework makes extending and maintaining the functionality of the benchmarking suite easier, as most of the framework’s code is shared across different modules. The solution was validated by first porting old scripts to Python using the new framework and then comparing them to scripts from the old benchmarking suite. The ported scripts are much simpler but retain the same functionality and benchmarking results.

2023

1. MSc

   Adapting an Alarm Repositioning Algorithm to Data Races

   Karoliine Holter

   University of Tartu, 2023

   Supervisors: Vesal Vojdani, Simmo Saan

   Abs HTML Code

   This master’s thesis addresses the challenge of enhancing the usability of sound static analyzers, specifically focusing on the state-of-the-art data race verifier Goblint. The aim is to soundly post-process the warnings generated by Goblint to make them more understandable for developers, thereby increasing the adoption of sound analyzers in practice. The thesis adapts and extends the warning repositioning algorithm of Muske et al. for data race warnings in multi-threaded C programs. Contributions include identifying and implementing a potential solution within the Goblint analyzer, extending the method for data races, and evaluating and analyzing the adapted algorithm in terms of the reduced distance between possible causes and warnings, as well as the impact on the quality of data race warnings.

2. BSc

   Abstract debugger for Goblint 🇪🇪

   Juhan Oskar Hennoste

   University of Tartu, 2023

   Supervisor: Simmo Saan

   Abs HTML Code

   Static analysis is a useful method for determining properties of programs without executing them. Goblint is a static analyser for the C programming language developed at the University of Tartu. During static analysis, Goblint determines many properties of the program, for example possible values of variables at different points in the program. These results are useful to understand the program being analysed, as well as the behavior of the Goblint analyses themselves. However, currently there is no good way to visualize them. Existing tools display the information in a raw and difficult to interpret form. In this thesis the initial version of one approach to visualize this information is implemented. The implemented approach is a special type of debugger, called an abstract debugger, which uses the same interface as a standard debugger, but instead of executing the program, it simulates program execution using the Goblint analysis results. The initial version of the abstract debugger is implemented and feedback for it is gathered from Goblint developers. The implemented abstract debugger is a step forward compared to existing tools for viewing Goblint analysis results.