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 a teams of 2-4) will be able to enhance Goblint with a new weakly relational domain i.e., a 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. 

The domain which is be implemented in the course of this practical is Logozzo et al. "Pentagons: A Weakly Relational Abstract Domain for the Efficient Validation of Array Accesses", OOPS 2008. (https://doi.org/10.1016/j.scico.2009.04.004)
This article presents an analysis that, in its basic setting, infers variable bounds, that is, valid inequalities of the form x ∈[a; b] or x < y for some constants a,b ∈ 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.