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 either

a) Implementing an abstract domain for floating point numbers

Cyber-Physical-Systems are becoming ubiquitous. Software is controlling robots, self-driving cars, and WiFi-enabled toothbrushes. Such programs heavily rely on floating point computations to model the continuous nature of the real world. While Goblint is state-of-the-art for the detection of data races and approaches for efficient yet precise analysis of multi-threaded programs, there is no meaningful abstract domain for floating points yet, limiting what Goblint can find out about such programs.

b)  Adding more expressive integer domains for making the detection of overflows more precise

Overflows of integer values are each programmer's mortal enemy. Static analyzers help avoiding these pitfalls. However, sound static analyzers may report so many potential overflows that programmers become overwhelmed. We would like to reduce the number of such false positives while still not missing any real ones by, e.g., enhancing Goblint with more sophisticated integer domains.

c) Tooling surrounding Goblint

Static Analysis is all in vain if the programmer cannot understand the results the analyzer presents and exploit them. We are developing a web-based frontend that allows for dynamically inspecting the findings of the analyses - sharing a code-base with the analyzer itself via compiling parts of it to JavaScript (using Js_of_ocaml). Your task will be to implement various improvements to make this web view even more dynamic and interactive.

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 developing a research prototype

Requirements:

• Program Optimization (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 was a pre-meeting on Feb 01, 2pm at: https://bbb.rbg.tum.de/mic-dya-2x9
There will be no pre-meeting for the second matching cycle, please consult the slides. If you fulfill the requirements and have questions, don't hesitate to reach out to us!
You can apply for this lab course on the matching plattform .