Software permeates all aspects of our daily life, and it is vital for programs used in critical situations to be free of bugs. In this seminar, we will study various approaches from the literature for Static Analysis of programs. Here, we are zoning in on one especially challenging problem, namely the analysis of concurrent programs and investigate recent (and not so recent) approaches from the literature.

Each student will be assigned a topic and will write a report. We will provide one paper per student as a starting point for further research.

A list of possible topics (spanning both Abstract Interpretation and Model Checking) includes:

• Miné: Relational thread-modular static value analysis by abstract interpretation. VMCAI ’14
• Farzan et al.: Stratified Commutativity in Verification Algorithms for Concurrent Programs. POPL '23
• He et al.: Satisfiability modulo ordering consistency theory for multi-threaded program verification. PLDI '21.
• Sharma and Sharma: Thread-modular Analysis of Release-Acquire Concurrency. SAS '21
• Jeannet: Relational interprocedural verification of concurrent programs. Software & Systems Modeling '13
• Gotsman et al.: Thread-modular shape analysis. PLDI '07
• S. et al.: Clustered Relational Thread-Modular Abstract Interpretation with Local Traces. ESOP '23

The seminar is organized as a mini-conference. After submitting your draft paper, you will be asked to review some drafts of your fellow students. You have the chance to incorporate this feedback before submitting the final version of the paper. The final talks will be held en-block within two or three days at the end of the semester.

Requirements:

• Be in your Master's
• Beyond this, there are no formal prerequisites, but the words "formal methods", "verification", "abstract interpretation" etc. should not scare you but rather inspire :)
• Write a letter of motivation (0.5 pages), attaching your Transcript of Records to julian.erhard@tum.de AND m.schwarz@tum.de using the title `[MSc Seminar]`.