Physics Department, TUM | Course 0000002014 in WS 2022/3

General Data

Course Type

practical training

Semester Weekly Hours

6 SWS

Organisational Unit

Informatics 2 - Chair of Formal Languages, Compiler Construction, Software Construction (Prof. Seidl)

Lecturers

Julian Erhard
Michael Schwarz
Responsible/Coordination: Helmut Seidl

Dates

1 singular or moved dates

iCalendar

	Date and Time	Room and Remark
!	Tue, 2022-07-19, 14:00–15:00	<a href="https://bbb.rbg.tum.de/mic-dya-2x9" rel="nofollow">https://bbb.rbg.tum.de/mic-dya-2x9</a>
!	Thu, 2023-02-09, 14:00–16:00	Boltzmannstr. 3 Abschlusspräsentation beider Goblint Praktika am i2

Assignment to Modules

IN2106: Master-Praktikum / Advanced Practical Course
This module is included in the following catalogs:
- Further Modules from Other Disciplines

Further Information

Courses are together with exams the building blocks for modules. Please keep in mind that information on the contents, learning outcomes and, especially examination conditions are given on the module level only – see section "Assignment to Modules" above.

additional remarks	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) 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. Your task will be to improve the overflow detection Goblint. In particular, you will implement an interval set domain, i.e. a domain that can keep track of multiple possible ranges for integer values. b) Termination Analysis Usually, we we want 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 occuring 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. c) Analyzing state-of-the-art C Code While the C language community is slow to adapat 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 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 - Deepen your functional programming skills - Give you insights into developing a research prototype There will be a joint pre-meeting for both Goblint practicals on July 19th, 2 p.m. at: https://bbb.rbg.tum.de/mic-dya-2x9
Links	TUMonline entry

additional remarks

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) 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. Your task will be to improve the overflow detection Goblint. In particular, you will implement an interval set domain, i.e. a domain that can keep track of multiple possible ranges for integer values. b) Termination Analysis Usually, we we want 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 occuring 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. c) Analyzing state-of-the-art C Code While the C language community is slow to adapat 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 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 - Deepen your functional programming skills - Give you insights into developing a research prototype There will be a joint pre-meeting for both Goblint practicals on July 19th, 2 p.m. at: https://bbb.rbg.tum.de/mic-dya-2x9

Links

TUMonline entry

Equivalent Courses (e. g. in other semesters)

Semester	Title	Lecturers	Dates
WS 2023/4	Practical Course - Static Analysis: Automated Bug Hunting and Beyond (IN0012, IN2106, IN4301)	Erhard, J. Schwarz, M. Responsible/Coordination: Seidl, H.	Thu, 13:00–15:00, MI 02.07.014 and singular or moved dates
SS 2023	Practical Course - Static Analysis: Automated Bug Hunting and Beyond (IN0012, IN2106, IN4301)	Erhard, J. Schwarz, M. Responsible/Coordination: Seidl, H.	singular or moved dates
SS 2022	Practical Course - Static Analysis: Automated Bug Hunting and Beyond (IN0012, IN2106, IN4301)	Erhard, J. Schwarz, M. Responsible/Coordination: Seidl, H.	singular or moved dates
SS 2021	Practical Course - Static Analysis: Automated Bug Hunting and Beyond (IN0012, IN2106, IN4301)	Erhard, J. Schwarz, M. Responsible/Coordination: Seidl, H.	singular or moved dates

Practical Course - Static Analysis: Automated Bug Hunting and Beyond (IN0012, IN2106, IN4301)

Course 0000002014 in WS 2022/3

General Data

Assignment to Modules

Further Information

Equivalent Courses (e. g. in other semesters)