Together with colleagues at the University of Tartu, we develop and maintain the Static Analyzer Goblint, that is based on Abstract Interpretation. The tool is capable of analyzing real-world C programs and show properties such as the absence of buffer overruns or data races in multi-threaded code. In the course of this practical, you (in teams of 2-4) will extend Goblint by implementing new analyses, e.g., for detecting dedicated classes of bugs or specific cases of Undefined behavior or work on tooling around it.

This will:

• Deepen your understanding of the semantics of C and typical programming errors
• Deepen your understanding of Static Analysis by Abstract Interpretation
• Deepen your functional programming skills
• Give some insights into a developing research prototype

Requirements:

• You should have taken the Program Optimization Course (IN2053) (or a similar course at another university)
• 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.

There will be a pre-meeting on Feb 3, 2 p.m. s.t., online at https://bbb.rbg.tum.de/mic-dya-2x9. You can apply for this lab course on the matching plattform .