Schedule Location Instructor
Lecture Tuesday,   16 - 18 c.t. E006, HGB Prof. Dr. Eyke Hüllermeier
Exercise A Thursday,  16 - 18 c.t. C113,  Theresienst. 41 Timo Löhr
Exercise B tba tba tba

The enrollment key is: Kolmogorov

In case of questions, please contact timo.loehr@ifi.lmu.de


Automated theorem proving is a subfield of mathematical logic that concerns itself with proving mathematical theorems fully automatically using computer programs. These programs are called automated theorem provers. They can be used as stand-alone programs to solve logic problems or in tandem with interactive theorem provers (also called proof assistants) to discharge proof obligations that arise in interactive proofs.

In this course, we will review some of the main approaches to automated theorem proving. The course focuses on the theory of theorem proving. Stylistically, the course has a mathematical flavor (with definitions, lemmas, proofs, etc.).

The course is based on the materials from Uwe Waldmann’s courses Automated Reasoning I and Automated Reasoning II at Saarland University. We are grateful to him for letting us use his materials.

Please enroll yourself for the course using this key: ATP2425

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

Enrolment key: pasec24

Enrollment Key: VerParProg 24/25

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

Compiler Construction


Access Code

The access code to this lecture is 'PriCoDe2425' (without leading and trailing ').


Description

In this course, students will learn the fundamental principles and techniques used in the design and implementation of compilers. The course covers the full compilation process, starting from lexical analysis, syntax analysis, and semantic analysis to code optimization and code generation.

Important Dates
  • Lecture: Tue 16 - 18, Room 027, Oettingenstraße 67
  • Tutorial: Fri 12 - 14, Room 027, Oettingenstraße 67

Key topics
  • Lexical Analysis: Tokenizing source code into meaningful symbols.
  • Syntax Analysis: Parsing tokens to form syntax trees and validate code structure using context-free grammars.
  • Semantic Analysis: Type checking and ensuring the correctness of meaning in programs.
  • Code Optimization: Techniques for improving code performance and reducing resource usage.
  • Code Generation: Translate intermediate representation of code to another language.

Exercises

Students will gain hands-on experience in building a simple compiler in a group project. The goal is to write a compiler and an interpreter for the BALAN language. Additionally, we will hand out weekly exercise sheets to prepare you for the exam at then end of the semester.


Prerequisites
  • Basic knowledge of data structures, algorithms, and programming languages. 
  • Familiarity with automata theory and formal languages is beneficial.
  • Beneficial Lectures: Formale Sprachen und Komplexität, Formale Spezifikation und Verifikation, Algorithmen und Datenstrukturen, Logik und Diskrete Strukturen.

Learning Outcomes
  • Understand the core components of a compiler.
  • Build a working compiler for the BALAN language.
  • Analyze and apply compiler optimizations to improve performance.
  • Gain insights into modern programming languages and their compilation techniques.

Enrolment key:

cMPy&m-!7r3zsk#?yZvQ

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: 5416


Course website: https://www.dbs.ifi.lmu.de/cms/studium_lehre/lehre_master/dma2425/index.html

Moodle Enrollment key: ZEa!g6e+A5Upm&kYQFh0

Content

The vast increase in data volume in almost every field results in increased difficulty or even impossibility for information analysis. Especially in areas such as biological measurement evaluation (e.g. gene sequencing, micro-array processes …) or data transaction in large telecommunications or network operators, using data without computational aid is inconceivable. The research area “Knowledge Discovery in Databases (KDD)” investigates solutions to these problems. It combines statistics, machine learning, database systems, and (semi-) automatic extraction methods for valid, new, and potentially useful knowledge from large databases. The term data mining in this context refers to the fundamental step in the KDD process, in which the actual analysis of the data is carried out. Data mining is often applied to large amounts of operational data that are managed separately in so-called data warehouses. The frequently used term Business Intelligence describes, among other things, the application of data mining algorithms to the information provided by a data warehouse in order to support targeted decision-making processes. The lecture gives an overview of the basics of the most important KDD techniques. Particularly: Classification, regression/trend detection, clustering, outlier detection, association rules, and process mining.

To deepen the lecture, exercises are offered in which the presented procedures are further explained and illustrated with practical examples.


Organization

Direction: Prof. Dr. Gabriel Marques Tavares (he/him)
Teaching Assistants:  


Planning

The following dates are tentative and minor changes are possible, so stay tuned.
EventTimePlaceBeginn
LectureWed, 09:15 - 11:45 Theoret. Hörsaal 151, Thalkirchner Str. 3616.10.2024
Exercise 1Thu, 12:00 - 14:00Lehrturm-VU104, Prof.-Huber-Platz 224.10.2024
Exercise 2 Thu, 14:00 - 16:00Lehrturm-VU104, Prof.-Huber-Platz 224.10.2024
Exercise 3Thu, 16:00 - 18:00Lehrturm-W201, Prof.-Huber-Platz 224.10.2024
Exercise 4Fr, 12:00 - 14:00Room E216, HGB25.10.2024


https://www.mobile.ifi.lmu.de/lehrveranstaltungen/intelligent-systems/

Computational Intelligence is the study of algorithms that exhibit (seemingly) intelligent behavior. Historically, it encompasses several fields of computer science, including logic, optimization, and multi-agent system. Our goal is to give the recently rapid developments in artificial intelligence a broader context by connecting them to their historical and scientific foundations. Thus, in this course we discuss intelligent system specified in an increasingly complex manner as well as relevant examples and literature.

Key to register: coin24

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
Termine
Vorlesung: Montags von 15 bis 18 Uhr c.t., Thalkirchner Str.36, Theoret. Hörsaal 151
  • Erster Termin: Mo, 14.10.2024
  • Letzter Termin: Mo, 27.01.2025

Hinweis: Den Einschreibeschlüssel für diesen Kurs erhalten Sie in der ersten Vorlesung.

Welcome to the course webpage for Parallel and High Performance Computing for winter-term 2024/25 at LMU Munich. Here you will find details on the lecture and the accompanying practical lab exercises.

Lecture slides will be made available chapter-by-chapter through this webpage.

Material from the lab exercises will be available via Moodle.

Here is the enrollment key: ParallelPioneers

Content

Parallel computing is concerned with using multiple compute units to solve a problem faster or with higher accuracy. Historically, the main application area for parallel machines is found in engineering and scientific computing, where high performance computing (HPC) systems today employ tens- or even hundreds of thousand compute cores.

The application area for parallel computing has, however, expanded recently to essentially include all areas of information technology. Virtually all servers, desktop, and notebook systems, and even smartphones and tablets are today equipped with CPUs that contain multiple compute cores. In each case, the potential for these systems can only be fully realized by explicit parallel programming. As such, understanding the benefits, challenges, and limits of parallel computing is increasingly becoming a "must have" qualification for IT professionals.

This course addresses the increasing importance of parallel and high performance computing and is covering three interwoven areas: Parallel hardware architectures, parallel algorithm design, and parallel programming. The successful student will be able to identify potentials for parallel computing in various application areas, judge the suitability of contemporary hardware architectures for a parallel computing problem and understand efficient implementation strategies using modern parallel programming approaches.

The lecture is partially based on material that has been developed at UC Berkeley and which has been funded by the US National Science Foundation. The course slides will be made available for download by the date of the lecture and will be in English.

Audience

The course is intended for both bachelor and master students of computer science and related fields. More formally, in German: Die Vorlesung richtet sich an Studenten der Informatik bzw. Medieninformatik (Diplom) nach dem Vordiplom sowie an Studenten der Informatik, Bioinformatik bzw. Medieninformatik (Bachelor, Master) im Rahmen der vertiefenden Themen der Informatik. Für Vorlesung und Übung werden 6 ECTS-Punkte vergeben.

Lab Exercises

The lecture is accompanied by a lab exercises to deepen the understanding of topics covered in the lecture. High performance computing systems hosted at the Leibniz Supercomputing Center will be made available to the students. Worksheets for the lab exercises will be made available on Moodle.

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.