teaching

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.