Praktikum - Static Analysis: Automated Bug Hunting and Beyond (IN0012, IN2106, IN4301)
Practical Course - Static Analysis: Automated Bug Hunting and Beyond (IN0012, IN2106, IN4301)
Lehrveranstaltung 0000002426 im SS 2023
Basisdaten
| LV-Art | Praktikum |
|---|---|
| Umfang | 6 SWS |
| betreuende Organisation | Informatik 2 - Lehrstuhl für Sprachen und Beschreibungsstrukturen in der Informatik (Prof. Seidl) |
| Dozent(inn)en |
Julian Erhard Michael Schwarz Leitung/Koordination: Helmut Seidl |
| Termine |
1 einzelner oder verschobener Termin |
Zuordnung zu Modulen
-
IN2106: Master-Praktikum / Advanced Practical Course
Dieses Modul ist in den folgenden Katalogen enthalten:- weitere Module aus anderen Fachrichtungen
weitere Informationen
Lehrveranstaltungen sind neben Prüfungen Bausteine von Modulen. Beachten Sie daher, dass Sie Informationen zu den Lehrinhalten und insbesondere zu Prüfungs- und Studienleistungen in der Regel nur auf Modulebene erhalten können (siehe Abschnitt "Zuordnung zu Modulen" oben).
| ergänzende Hinweise | 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 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 your own static analysis. Possible topics include: a) Termination Analysis Usually, we want to be sure that our programs terminate. The Halting Problem states that deciding whether a program terminates or not is not possible in all cases. However, in benign cases, one can show that all loops occurring in a program are only iterated a finite number of times. One approach to do this is to add an additional variable, that is incremented in each iteration of the loop. If the static analyzer is able to prove that the value range for this variable has an upper bound, the loop is proven to be terminating. For programs that contain procedure calls, one has to additionally show that no infinite recursion is possible. Your task will be to implement an analysis that is able to prove termination of loops, and checks the call graph for cycles. As a result, your analysis will be able to show termination for suitable programs. b) Analyzing state-of-the-art C Code While the C language community is slow to adapt new standards, usage of features introduced in C11 is on the rise. While Goblint has full support for C99 features, the support for analyzing programs written in C11 is incomplete. In particular, C11 introduced features for multithreading, including standard functions for thread creation, joining, as well as thread local variables. These features are of particular interest for us, as one of the core strengths of Goblint that sets us apart from many competitors in the same field is the analysis of multithreaded (pthread) programs. Your task will be to implement support for the analysis of code that uses C11 features, in particular related to the C11 multithreading library. Participating in this practical course 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 There will be a pre-meeting for the Goblint practical on Feb 7, 1 p.m. at: https://bbb.rbg.tum.de/mic-dya-2x9 |
|---|---|
| Links | TUMonline-Eintrag |
Gleiche Lehrveranstaltungen (z. B. in anderen Semestern)
| Semester | Titel | Dozent(en) | Termine |
|---|---|---|---|
| WS 2023/4 | Practical Course - Static Analysis: Automated Bug Hunting and Beyond (IN0012, IN2106, IN4301) |
Erhard, J.
Schwarz, M.
Leitung/Koordination: Seidl, H. |
Do, 13:00–15:00, MI 02.07.014 sowie einzelne oder verschobene Termine |
| WS 2022/3 | Practical Course - Static Analysis: Automated Bug Hunting and Beyond (IN0012, IN2106, IN4301) |
Erhard, J.
Schwarz, M.
Leitung/Koordination: Seidl, H. |
einzelne oder verschobene Termine |
| SS 2022 | Praktikum - Static Analysis: Automated Bug Hunting and Beyond (IN0012, IN2106, IN4301) |
Erhard, J.
Schwarz, M.
Leitung/Koordination: Seidl, H. |
einzelne oder verschobene Termine |
| SS 2021 | Practical Course - Static Analysis: Automated Bug Hunting and Beyond (IN0012, IN2106, IN4301) |
Erhard, J.
Schwarz, M.
Leitung/Koordination: Seidl, H. |
einzelne oder verschobene Termine |