Siehe TUMonline

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.

We recommend that you have taken the Program Optimization Course
(IN2053) (or a similar course) 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)