Master's Courses in WiSe 23/24


Seminar: Prozessorientiertes IT-Service-Management WiSe 23/24

Advanced Topics in Computer Graphics WiSe 23/24

The lecture will cover the following topics:

    The course will provide an overview of advanced topics in computer graphics not currently covered by other LMU courses. In particular:
    • Emphasis on real-time algorithms suitable for videogames or interactive exploration of virtual worlds.
    • Realistic graphics: Advanced effects not present in off-the-shelf solutions; physical phenomena and implementation possibilities as algorithms.
    • Non-photorealistic graphics (for illustrations or for artistic effects); especially real-time effects.
    • Introduction to proofs of computational time limits and convergence to the correct solution.
    • Remote visualization advantages, disadvantages and implementation details.
    • Virtual reality: Caveats and available resources (content of course orthogonal to the subject Virtual Reality (2019, Vorlesung; 2021, Praktikum).
    • Applications in Serious games.

Affective Computing WiSe 23/24

Algorithmen auf Sequenzen WiSe23/24

Arbeitsgemeinschaft Quanten Computing WiSe 23/24

Seminar zu Quantenthemen am Lehrstuhl für mobile und verteilte Systeme. Hier werden aktuelle Forschungsthemen unseres Lehrstuhls vorgestellt und diskutiert.

Über das Seminar können auch Bachelor- und Masterarbeiten vergeben werden.

Arbeitsgemeinschaft Artificial Intelligence Wise 23/24

Blockpraktikum Quantencomputing WiSe 2023/24

Automated Algorithm Configuration and Design WiSe 23/24

Many real-world applications entail difficult problems to be solved such as Boolean satisfiability (SAT), constraints satisfaction problems (CSP), finding a proper machine learning model for a given data set, or performing highly complex simulations. Typically, in these domains, there is not just a single algorithm that performs best across all instances of the respective problem. Instead, various algorithms exist that are more or less suitable for specific problem instances. To this end, automated algorithm configuration and design automates the design of what algorithm (configuration) to choose for which problem instance. This course will provide an overview of the are of automated algorithm configuration and design, discuss problem variants as well as methods tackling these problems.

General introduction to automated algorithm configuration and design
- Algorithm Selection
- Algorithm Composition
- Programming by Optimization
- Dynamic versus Static Algorithm Configuration
- Benchmarking

Prerequisites:
- Knowledgeable in machine learning
- Programming skills

The course enrolment key: AACD2023/24

Computational Intelligence WiSe 23/24

Das Feld der Computational Intelligence beschäftigt sich mit Algorithmen, die vermeintlich intelligentes Verhalten umsetzen. Im Rahmen dieser Vorlesung werden simple Algorithmen zur Entscheidungsfindung sowie moderne Techniken der künstlichen Intelligenz betrachtet. Ein besonderer Fokus wird dabei auf verteilte Intelligenz und Multi-Agenten-Systeme gelegt.

Schlüssel zur Selbseinschreibung: "CoInWiSe2324!" (ohne "")

Data Mining Algorithmen I (DMA I) WS 2023/24

aka Knowledge Discovery in Databases I (KDD I)

Deep Learning and Artificial Intelligence WiSe 23/24

During the last decade, the availability of large amounts of data and the substantial increase in computing power allowed a renaissance of neural networks and advanced planning techniques for independent agents. Whereas deep learning extended well-established neural network technology to allow a whole new level of data transformation, modern reinforcement learning techniques yield the artificial backbone for intelligent assistant systems and autonomous vehicles. The course starts with an introduction to neural networks and explains the developments that led to deep architectures. Furthermore, the course introduces advanced planning techniques and how they can be trained using deep neural networks and other machine learning technologies.

The Key for course enrolment: 6AJbipmE0Y4U0r-hSrZ&

Grid und Cloud Computing WiSe 2023/24

Grids und Clouds stellen unterschiedliche Ausprägungen eines verteilten Informatikparadigmas dar, durch das unter Ausnutzung von geographisch und administrativ verteilten Systemen im Bedarfsfall ein Pool von Ressourcen und abstrakten, virtualisierten und dynamisch-skalierbaren Services (z. B. Rechenleistung, Speicherkapazität, Plattformen, Visualisierung) über das Internet bereitgestellt wird.

In dieser Vorlesung (und den begleitenden Übungen) werden die Grids und Clouds zu Grunde liegenden Fragestellungen und Technologien vorgestellt und praktisch angewandt. Nach einer ausführlichen Motivation werden zunächst grundlegende verteilte Systemmodelle und Basistechnologien betrachtet. Darauf aufbauend werden folgende Themen behandelt: Cloud-Architekturen, Cloud-Programmierung und Software-Umgebungen (Workflows, MapReduce, Spark, Google Cloud Dataflow, Amazon AWS, Data Lakes, etc.), Virtuelle Organisationen, Grid Computing-Umgebungen, Resource Management, Data Management, Ubiquitous Computing mit Clouds und im Internet of Things, Grids of Clouds, Clouds of Grids. 
Abschließend werden spezielle Fragestellungen zu Realzeitaspekten, wie sie zum Beispiel im Urgent Computing auftreten, und neue Trends behandelt.

Die Vorlesung richtet sich vornehmlich an Master-Studenten, die sich mit neueren Entwicklungen im verteilten Hochleistungsrechnen (Systemarchitektur, Programmierparadigmen, Leistungseffizienz, Energieeffizienz) vertraut machen wollen.

Der Relevanz des Themas wird durch Gastbeiträge externer Experten Rechnung zu tragen. Diese Vorträge werden teilweise in englischer Sprache gehalten.


Intelligent Systems WiSe 23/24

IT-Sicherheit WiSe 23/24

Mit der rasanten Verbreitung von Netztechnologien und -diensten sowie deren Durchdringung des privaten wie des geschäftlichen Bereichs steigt der Bedarf an sicheren IT-Systemen. Immer häufiger auftretende Angriffe auf vernetzte IT-Systeme mit zum Teil extrem hohem wirtschaftlichen Schaden für die betroffenen Firmen verdeutlichen den Bedarf nach wirksamen Sicherheitsmaßnahmen.

Diese Vorlesung beschäftigt sich mit ausgewählten Sicherheitsanforderungen und -mechanismen und deren Umsetzung in verteilten Systemen. Themen sind unter anderem:

  • Information Security Management (ISO/IEC 27001)
  • Bedrohungen und Angriffe
  • Kryptographische Algorithmen
  • Sicherheitsmechanismen und deren Realisierung
  • Netz-Sicherheit

Machine Learning WiSe23/24

Self-enrollment key: X+1FxqZh@?9zeRqr0GgW

Master Practical: Image & Video Synthesis WiSe 23/24

Time and Place: TBD
6 SWS
Modern Deep Learning has fundamentally changed Artificial Intelligence. Novel applications as well as significant improvements to old problems continue to appear at a staggering rate. Especially the areas of image and video understanding, retrieval, and synthesis have seen tremendous improvements and even the human baseline has been outperformed in several difficult applications.

The algorithms and the fundamental research in deep Machine Learning and Computer Vision that are driving this revolution are improving at an ever-increasing rate. The goal of this practical lab is, therefore, to give students hands-on experience with the state-of-the-art in this field of research. We will work on current problems in Computer Vision and Machine Learning and build on current algorithms to practically implement novel solutions. Consequently, the practical is also a good opportunity to take a close look at this area of research and prepare for a potential future final thesis.

Topics include but are not limited to:
* Image & video synthesis
* Visual superresolution and Image completion
* Artistic style transfer
* Interpretability of deep models
* Visual object classification, detection, tracking
* Self-supervised learning
* Metric and representation learning
* Modern deep learning approaches, such as transformers and self-attention, invertible neural networks, etc.
* …

Institut
Institut für Informatik

Master Practical: Visual Representation Learning WiSe 23/24

Time and place: TBD

Oberseminar: High-level Vision WiSe 23/24

Oberseminar Technology-Enhanced-Learning

Das Oberseminar ist die wichtigste Kommunikationsplattform für die Forschungsinteressen der Mitglieder des Forschungsgruppe “Technology-Enhanced Learning”. Hier werden Informationsveranstaltungen für Bachelor- und Masterstudierende abgehalten, über den Antritt und den Abschluss von Studienarbeiten berichtet, die Mitarbeiter der Arbeitsgruppe informieren über ihre Forschung und renommierte Wissenschaftler aus dem In- und Ausland dozieren zu Forschungsthemen, die für die Gruppe von Interesse sind.

Melden Sie sich bitte über diese Seite für das Oberseminar an, um Einladungen zu den Vorträgen und Anweisungen zu erhalten! Das Seminar wird in Präsenz stattfinden, eine alternative Teilnahme über Zoom ist ebenfalls möglich.

Einschreibeschlüssel: TEL

Online Machine Learning and Bandits WiSe 23/24

Parallel and High Performance Computing WiSe 23/24

Autonome Systeme Praktikum WiSe 23/24

Moderne Systeme - z.B. Roboter - agieren autonom: Sie treffen selbstständig Entscheidungen und passen Ihr Verhalten flexibel den aktuellen Umständen und Anforderungen an. In diesem Praktikum beschäftigen wir uns mit der Umsetzung autonomer Systeme. Wir implementieren Algorithmen zur adaptiven Planung, Optimierung und Koordination sowie Methoden zur Evaluation und Analyse autonomer Systeme. Eine Auswahl der behandelten Themen lautet:

  • Decision Making in Autonomous Systems
  • Planning and Reinforcement Learning
  • Simulation and Approximation

Praktikum: Administration und Konzeption virtueller Systeme WiSe 23/34

Das Blockpraktikum bildet eine theoretische und praktische Einführung in die Administration und Konzeption virtueller Systeme. Unter Laborumgebung wird die Installation, Konfiguration und Administration von Virtuellen Systemen anhand Softwarelösungen von VMware durchgeführt.

Inhalte

Inhalt der Lehrveranstaltung sind Installation, Konfiguration und Management von VMware vSphere 7.0

  • Course Introduction
  • Introduction to vSphere and the Software-Defined Data Center
  • Virtual Machines
  • vCenter Server
  • Configuring and Managing Virtual Networks
  • Configuring and Managing Virtual Storage
  • Virtual Machine Management
  • Resource Management and Monitoring
  • vSphere Clusters
  • vSphere Lifecycle Management

Das Praktikum enhält Vorlesungsanteile und praktische Übungen.

Prüfung

Die Prüfung zur Veranstaltung findet voraussichtlich am 16.-18.10.2023 anhand praktischer Aufgaben und deren Präsentation statt. Details werden während der Veranstaltung bekannt gegeben.

Zertifizierung

Das Seminar erfüllt die Zulassungsvoraussetzung zu den Industrie Zertifizierungen

  • VMware Certified Associate (VCA) und
  • VMware Certified Professional (VCP).

Teilnehmer

Das Praktikum richtet sich an Master- und Bachelor-Studenten der Informatikstudiengänge.
Kurssprachesprache: Deutsch, Kursmaterial Englisch.

Die Anmeldung erfolgt über Moodle. Der Einschreibeschlüssel lautet "vSphere".

Die Veranstalltung ist ein Blockpraktikum, wird jedoch als Semester-Wochenstunden (V+Ü) 2+2 angerechnet.

Voraussetzung für die Teilnahme

Vorlesung "Rechnernetze und Verteilte Systeme", Vorlesung "Virtualisierte Systeme" von Vorteil.

Ort

Oettingenstrasse 67, Hörsaal 057

Termine

Montag, 09.10.2023 - Freitag, 13.10.2023: 09:00 - 18:00 Uhr

Unterlagen

Die Kursunterlagen werden bei Kursbeginn ausgehändigt.
Ein Notebook / Tablet mit aktuellem Browser ist zur Bearbeitung der praktischen Aufgaben erforderlich.

Praktikum: Quantum Computing Programmierung WiSe 23/24

Praktikum: Evaluierung moderner HPC-Architekturen und -Beschleuniger WiSe 23/24

Program Analysis for Security WiSe 23/24

Summary: This course deals with applying formal methods for reasoning about programs to low-level code (such as x86 machine code) to find bugs, prove their absence, or simply gain more information about software (reverse engineering).

Topics we intend to cover include:

  • Executable formats and machine code
  • Disassembly and decompilation
  • Classic dataflow analysis, theory and practice
  • Recovering control flow
  • Fuzzing (mutation-based, grammar-based)
  • Debugging and dynamic binary instrumentation
  • Taint analysis and symbolic execution

Lectures: Wednesday, 13:00 - 16:00, Amalienstr. 73A / 218

Exercises: Monday, 14:00 - 16:00, Amalienstr. 73A / 218

Enrolment key: pasec23

SAT Solving WiSe 23/24

Einschreibeschlüssel: SAT_WS23-24

Seminar: Algorithms for Model Checking WiSe 23/24

Basic Information

  • Language: English
  • Prerequisite courses
    • Formal Languages and Complexity (must)
    • Logic and Discrete Structures (must)
    • Formal Specification and Verification (recommended)
    • Software Verification (recommended)
    • SAT Solving (recommended)
  • Date: Thursday, 16:15-17:45
  • Location: Seminar Room 067, Oettingenstr. 67
  • First meeting: 2023-10-19 (about the detailed seminar organization and expectations)
    • IMPORTANT: Absence from the first meeting will lead to a failing grade in the seminar.

Content

Model checking is an important research field in computer science where automatic solutions to the following problem are studied: Given a computing model and a specification, decide whether the model satisfies the specification or not. In practice, a computing model can be a digital circuit (hardware) or a program (software). A specification can be a safety property requiring that errors never happen during the execution of the computing model. Compared to testing, model checking can guarantee the correctness of computing systems with mathematical rigor. Model checking is rooted in a solid theoretical foundation and requires advanced software engineering for tool implementation. The inventors of model checking won the 2007 Turing Award, and leading technology companies use model-checking techniques to assure the quality of their products.

Goal

The goal of this seminar is to learn the mathematical foundation and understand the working of state-of-the-art algorithms for hardware and software model checking. At the end of this seminar, students should become familiar with the background knowledge of model checking and able to explain a scientific publication on model checking in oral and written forms.

Organization

The seminar will consist of three phases:

  1. Reading lectures: In the first phase, we will recap the mathematical foundation of model checking. Students will be divided into groups. Each group will be assigned a topic and lead the discussion on the topic in one seminar session.
  2. Weekly group meetings: In the second phase, each student will be assigned a publication on an algorithm for model checking. Students will have weekly meetings with the mentors to report their progress. Mentors will guide students to read and understand the algorithms in the publications.
  3. Final presentation and report: In the final phase, students will present the algorithms assigned to them and write a report explaining them with examples and analysis.

Team

References

Seminar: Ethik der Künstlichen Intelligenz WiSe 23/24

Seminar: Foundation Models in Artificial Intelligence WiSe 23/24

Seminar: Functional Programming and Type Theory WiSe 23/24

Seminar: Gödel's Incompleteness Theorems WiSe 23/24

Gödel's incompleteness theorems are celebrated results in mathematical logic that significantly impact on computing. A seminar's first aim is to get a grasp of Gödel's incompleteness theorems' proofs. A seminar's second aim ist to directly approach Gödel's incompleteness theorems from Gödel's article of 1938, helped if needed from introduction to (modern version of) the proofs of Gödel's incompleteness theorems. The seminar's third and last aim ist to grasp the meaning of Gödel's incompleteness theorems - and to debunk some widespread esoteric "understandings" of these theorems. 

Seminar: IoT Security WiSe 23/24

Seminar: Machine Ethics WiSe 23/24

Machine Ethics investigates how to ensure the ethical behaviour of artificial intelligent agents, that is, machines that rely on artificial intelligence. Machine ethics has been considered since the middle of the 20th century. It has been popularized through the Three Law of Robotics postulated by Isaac Asimov in his 1942 science fiction short story "Runaround" (re-published in 1950 in Asimov's short story collection "I, Robot"). Machine ethics has gained momentum as a sub-field of Computing Ethics since the beginning of the 21th century following the proliferation of Artificial Intelligence tools. 

The master seminar aims at introducing to machine ethics – stressing the engineering of ethical machines. 

Seminar: Machine Learning for Knowledge Graphs WiSe 23/24

Seminar: Modellierung dynamischer und adaptiver Systeme WiSe 23/24

❗Bitte beachten Sie die kürzlich geänderten und weiter unten angegebenen Termine!❗

Anmeldung

Sie können an diesem Seminar sowohl für Bachelor als auch für Master teilnehmen. Die Anmeldung zu diesem Seminar erfolgt über die Zentralanmeldung. Bitte beachten Sie unbedingt die Hinweise zur Anrechnung weiter unten!

Benötigte Kenntnisse für das Seminar: Softwaretechnik

Lernziele:

  • Kenntnis der Methoden und Verfahren zur Beschreibung, Modellierung und Simulation dynamischer Systeme
  • Vertrautheit mit den Besonderheiten solcher Systeme, mit Simulationsprogrammen und mit Anwendungsfeldern außerhalb der Informatik.

Inhalt:

  • Methoden und Verfahren zur Beschreibung, Modellierung und Simulation dynamischer Systeme.
  • Betrachtung der Besonderheiten solcher Systeme wie dynamische Einflussgrößen, Rückkopplungsschleifen, Stabilität bzw. Instabilität.
  • Anwendungen: Zum Beispiel aus der Steuerungstechnik, aus Psychologie und Soziologie (Simulation und Steuerung sozialer Systeme), den Wirtschaftswissenschaften (Steuerung ökonomischer Systeme), der Umweltforschung und der Entwicklung von Spielen.

Im Seminar werden Beschreibungsmethoden und Simulationsprogramme für dynamische Systeme behandelt und an Anwendungsbeispielen aus verschiedenen Disziplin

Seminar-Leitung

Prof. Dr. Martin Wirsing, Prof. Dr. Wolfgang Hesse

Technische Fragen: Dr. Philipp Wendler

Termine und Ablauf

Das Seminar findet zu Beginn des Semesters wöchentlich statt, jeweils Donnerstags 12-14 Uhr., und beginnt mit dem ersten Termin am 09.11.2023 (❗). Die studentischen Vorträge erfolgen als Blockveranstaltung an zwei Samstagen (❗).

  •  Einführungsveranstaltung (09.11.2023❗)
  •  Vorträge zum Thema (16.11., 23.11., 30.11.2023)
  • Studentische Vorträge ( Samstag, 09.12.2023 und 20.01.2024 9-18 Uhr ❗)
  • Abschlussveranstaltung (25.01.2024)
Im Oktober sowie am 02.11.2023 sind keine Seminartermine.

Anrechnung

Die Lehrveranstaltung findet in einer gemischten Form statt, bestehend aus Vorlesungsanteilen und Seminarvorträgen statt. Sie kann im Hauptfach Informatik/Medieninformatik folgendermaßen angerechnet werden:

  • Das Seminar kann als Bachelorseminar angerechnet werden. Dieses gibt nur 3 ECTS-Punkte. Gefordert sind dafür laut Prüfungsordnung eine Hausarbeit mit 7.000-14.000 Zeichen sowie eine mündliche Prüfung von 30-45 Minuten. Der Seminarvortrag zählt als mündliche Prüfungsleistung. Melden Sie sich in diesem Fall über die Zentralanmeldung für Bachelorseminare an.
  • Das Seminar kann als Masterseminar angerechnet werden. Dieses gibt dann 6 ECTS-Punkte. Gefordert sind dafür laut Prüfungsordnung natürlich etwas mehr: Hausarbeit mit 20.000-30.000 Zeichen sowie eine mündliche Prüfung von 30-45 Minuten. Auch hier zählt der Seminarvortrag als mündliche Prüfungsleistung. Melden Sie sich in diesem Fall über die Zentralanmeldung für Masterseminare an.
  • Das Seminar kann als Veranstaltung für Vertiefende Themen der Informatik für Bachelor angerechnet werden. Dieses gibt ebenfalls 6 ECTS-Punkte. Gefordert werden dabei die gleichen Leistungen wie für das Masterseminar. Melden Sie sich in diesem Fall über die Zentralanmeldung für Masterseminare an.

Seminar: Recent Development in Multi-Modal Models WiSe 23/24

Our world and perception consist of various modalities ranging from image, video, sound, and text to senses, which make a complete picture of our surroundings. Similarly, recent trends in deep learning focus on multi-modal data beyond Vision and NLP models. Current advancement of large multi-modal like Pali[1], ImageBind[2], and Segment Anything[3] shows visual features conjugation with text, depth, and 3D features, showing remarkable robustness and scalability across domains. A large model like Pali-X shows extraordinary abilities to understand images, videos, and documents and could achieve state-of-the-art results on OCR, VQA, and few or zero-shot generalizations. On the other hand, models like Segment Anything could detect thousands of concepts based on user prompts.  

This seminar will explore various multimodal model and the recent trends ranging from their architecture, training, and type of modality. We will also study their advantage and how they can be more generalizable toward a seen/unseen in-context understanding of their prospects. 

Please note that it is a Block seminar and will start or have a first meeting on January 25 (16:00 to 17:30); the initial introduction or group will be created on February 8th (16:00 to 17:30), and the final presentation will take place on March 5th. Place: DBS conference room 157

[1] Chen, Xi, et al. "PaLI: A Jointly-Scaled Multilingual Language-Image Model" *arXiv preprint arXiv:2209.06794* (2023).

[2] Kirillov, Alexander, et al. "Segment Anything." *arXiv preprint arXiv:2304.02643* (2023).

[3] Girdhar, Rohit, et al. "Imagebind: One embedding space to bind them all." Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition. 2023.

[4] Ye, Qinghao, et al. "mplug-owl: Modularization empowers large language models with multimodality." arXiv preprint arXiv:2304.14178 (2023).


Seminar: Reproducibility of Software Engineering Research WiSe 23/24

Content

A good amount of software-engineering research consists of the creation of software or its analysis. The software and data that are created by researchers in this process are referred to as "research artifacts". These artifacts are useful in two ways. First, other researchers can reproduce the reported research results. That means that, in theory, anyone having access to the research artifact should be able to observe the same results as reported by the researchers. Second, other researchers can reuse these artifacts in their own research.

The goal of this seminar is to learn how to use and assess artifacts from software engineering and programming language research.

In this process students will acquire basic skills for conducting reproducible scientific re­search, which will be useful for their final projects and further academic careers. They will learn how to perform a reproduction study, document their work, write a report, and present their findings.

Students will perform a reproduction study on a given set of already published artifacts. Their main tasks are to

  • verify that published research artifacts are still available and usable,
  • read the related publications,
  • follow the documentation of the artifacts to reproduce the studies' results, and
  • report the findings.

Team

Process

This presence course will consist of 3 phases.

  1. Reading lectures: four presence sessions (one per week) in which students will read and discuss relevant publications on artifact evaluation to gain knowledge on the topic and relevant skills to perform the reproduction study.

  2. Reproduction study: independent work in which each student is given a set of publications with artifacts. Students will document their independent work in lab reports and present the individual reproduction results. A weekly office hour will be offered for discussions on practical issues that students may be facing.

  3. Report and presentation: Students will write a final report based on their experimental work documented in the lab report from phase 2. Additionally, they will prepare a 10 minutes presentation.

Requirements

Students should be interested in reading and understanding scientific publications. A healthy degree of scepticism is beneficial.

This seminar is in English.


Seminar: Vertiefte Themen in Mobilen und Verteilten Systemen WiSe 23/24

Technology-Enhanced Learning WiSe 23/24

Einschreibeschlüssel: TEL

Technology-Enhanced Learning (TEL) describes the integration or application of technologies in the context of teaching and learning.

This master lecture gives an overview of e-learning topics from the perspective of computer science. General didactic scenarios and learning theories are discussed first. Based on this theoretical basis, tools, platforms, architectures and standards as well as special use cases (e-assessment, mobile learning, collaborative learning and the like) are covered. Furthermore, related non-technical aspects such as organization, rights, business models, etc. are discussed.

The lecture will be held in presence.

Form of examination: Written or oral examinations

Uncertainty in Artificial Intelligence and Machine Learning WiSe 23/24


Schedule Location Instructor
Lecture Tuesday,   16 - 18 c.t. E006, HGB Prof. Dr. Eyke Hüllermeier
Exercise A Thursday,  16 - 18 c.t. M109,  HGB Yusuf Sale
Exercise B TBA TBA Yusuf Sale

The enrollment key can be found on the corresponding uni2work homepage.

In case of questions, please contact yusuf.sale@ifi.lmu.de 


Verification of Parallel Programs WiSe 23/24

Enrollment Key: VerParProg 23/24

The course deals with mostly automatic verification approaches for multi-threaded programs with shared memory. Topics of the course are:

  • Semantics of parallel programs, e.g., interleaving semantics
  • Static and dynamic approaches for data race detection
  • Techniques for deadlock detection
  • Verification of program properties (e.g., with sequentialization, bounded model checking, etc.)
  • Partial Order Reduction
  • Thread-modular verification

At the end of the course, students can name a number of techniques for the verification of parallel programs, especially in the area of data race and deadlock detection as well as for verification of safety properties. They should be able to explain the underlying formalisms of the techniques, to describe the work flow of the different techniques, and to apply the techniques on examples. Moreover, the students know the strengths and weaknesses of the techniques.

Literature

Program Semantics

  • K. R. Apt, F. S. de Boer, E.-R. Olderog: Verification of Sequential and Concurrent Programs. Springer 2009.

Data Race Detection

  • S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, T. E. Anderson: Eraser: A Dynamic Data Race Detector for Multi-Threaded Programs. SOSP 1997.
  • E. Poznianski, A. Schuster: Efficient On-the-Fly Data Race Detection in Multithreaded C++ Programs. IPDPS 2003.
  • C. Flanagan, S. N. Freund: FastTrack: efficient and precise dynamic race detection. PLDI 2009.

Deadlock Detection

  • Dawson R. Engler, Ken Ashcraft: RacerX: effective, static detection of race conditions and deadlocks. SOSP 2003.
  • Mayur Naik, Chang-Seo Park, Koushik Sen, David Gay: Effective static deadlock detection. ICSE 2009.

Sequentialization

  • Akash Lal, Thomas W. Reps: Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis. CAV 2008.
  • Omar Inverso, Ermenegildo Tomasco, Bernd Fischer, Salvatore La Torre, Gennaro Parlato: Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization. CAV 2014.

Bounded Model Checking

  • L. C. Cordeiro, B. Fischer: Verifying multi-threaded software using SMT-based context-bounded model checking. ICSE 2011

Thread-modular Verification

  • C. Flanagan, S. N. Freund, S. Qadeer: Thread-Modular Verification for Shared-Memory Programs. ESOP 2002

Partial Order Reduction

  • D. Peled: Partial-Order Reduction. Handbook of Model Checking 2018.
  • P. Godefroid, D. Pirottin: Refining Dependencies Improves Partial-Order Verification Methods (Extended Abstract). CAV 1993.
  • P. Godefroid, P. Wolper: Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties. Formal Methods in System Design 2(2) 1993.

Atomicity Checking

  • C. Flanagan, S. N. Freund: Atomizer: a dynamic atomicity checker for multithreaded programs. POPL 2004


Virtual Reality WiSe 23/24