Together with colleagues at the University of Tartu, we develop and maintain the Static Analyzer Goblint, which is based on Abstract Interpretation.
The tool is capable of analyzing real-world C programs and showing properties such as the absence of buffer overruns or data races in multi-threaded code without requiring any user interaction at all. Goblint won the Data Race Category of the Software Verification Competition in 2023.

In the course of this practical, you (in teams of 2-4) will be able to enhance Goblint with new relational domains, i.e., domains tracking not abstractions of one variable but relationships between multiple variables. Such domains are useful, e.g., for detecting buffer-overflows where neither the index's exact value nor the array's length is known beforehand. This topic lies at the intersection of the expertise of our research group, i.e., it is supervised by an expert on numerical relational domains and contributors to the Goblint static analyzer.

One of the domains which may be implemented in the course of this practical is Flexeder et al. "Fast interprocedural linear two-variable equalities", TOPLAS 2012. (https://doi.org/10.1145/2049706.2049710)
This article presents an analysis that, in its basic setting, infers all valid variable differences, that is, all valid equalities of the form x = c or x = y+c for some constant c ∈ Z.

This will:

• Deepen your understanding of the semantics of C and typical programming errors
• Deepen your understanding of static analysis by Abstract Interpretation
• Level up your functional programming skills
• Become connected to the research we do day-to-day

Requirements:

• We recommend that you take the Program Optimization Course (IN2053) (or a similar course at another university) before doing this practical
• Knowledge of a functional programming language (we use OCaml, but the basics are not so different from other functional programming languages)
• Be in your Master's (Advanced Bachelor's students welcome)

Schedule

This course will stretch over most of the lecture time. On top of working in your team, you will have weekly to biweekly meetings with us. At the end of the practical all teams will present their results. We expect you to attend and participate in the Q&A.