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
- Trainer/in: Eyke Hüllermeier
- Trainer/in: Timo Löhr
- Trainer/in: Yusuf Sale
- Trainer/in: Volker Heun
- Trainer/in: Caroline Friedel
- Trainer/in: Katharina Reinisch
- Trainer/in: Elena Weiß
- Trainer/in: Jan Johannsen
- Trainer/in: Luca Maio
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
- Trainer/in: Jasmin Blanchette
- Trainer/in: Lydia Kondylidou
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
- Trainer/in: Tristan Benoit
- Trainer/in: Oliver Braunsdorf
- Trainer/in: Moritz Dannehl
- Trainer/in: Matias Gobbi
- Trainer/in: Sebastian Jänich
- Trainer/in: Johannes Kinder
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
- Trainer/in: Max Barth
- Trainer/in: Marie-Christine Jakobs
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.
- Trainer/in: Daniel Baier
- Trainer/in: Dirk Beyer
- Trainer/in: Matthias Kettl
Enrolment key:
cMPy&m-!7r3zsk#?yZvQ
- Trainer/in: Volker Tresp
- Trainer/in: Gengyuan Zhang
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
- Trainer/in: Maximilian Bernhard
- Trainer/in: Matthias Schubert
- Trainer/in: Niklas Strauß
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:
- Tanveer Hannan (he/him)
- Mamdouh Aljoud (he/him)
Planning
The following dates are tentative and minor changes are possible, so stay tuned.Event | Time | Place | Beginn |
---|---|---|---|
Lecture | Wed, 09:15 - 11:45 | Theoret. Hörsaal 151, Thalkirchner Str. 36 | 16.10.2024 |
Exercise 1 | Thu, 12:00 - 14:00 | Lehrturm-VU104, Prof.-Huber-Platz 2 | 24.10.2024 |
Exercise 2 | Thu, 14:00 - 16:00 | Lehrturm-VU104, Prof.-Huber-Platz 2 | 24.10.2024 |
Exercise 3 | Thu, 16:00 - 18:00 | Lehrturm-W201, Prof.-Huber-Platz 2 | 24.10.2024 |
Exercise 4 | Fr, 12:00 - 14:00 | Room E216, HGB | 25.10.2024 |
- Trainer/in: Mamdouh Aljoud
- Trainer/in: Tanveer Hannan
- Trainer/in: Benjamin Heilein
- Trainer/in: Gabriel Marques Tavares
- Trainer/in: Thomas Seidl
- Trainer/in: Jannik Wiese
https://www.mobile.ifi.lmu.de/lehrveranstaltungen/intelligent-systems/
- Trainer/in: Michael Kölle
- Trainer/in: Jonas Nüßlein
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
- Trainer/in: Thomas Gabor
- Trainer/in: Claudia Linnhoff-Popien
- Trainer/in: Maximilian Zorn
- Trainer/in: Dieter Kranzlmüller
- Trainer/in: Elisabeth Mayer
- Trainer/in: Thomas Odaker
- Trainer/in: Ruben Garcia-Hernandez
- Trainer/in: Dieter Kranzlmüller
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
- Erster Termin: Mo, 14.10.2024
- Letzter Termin: Mo, 27.01.2025
- Trainer/in: Amineh Akhavan Saraf
- Trainer/in: Manfred Buchner
- Trainer/in: Marcel Buggele
- Trainer/in: Kathrin Garb
- Trainer/in: Helmut Reiser
- Trainer/in: Daniel Weber
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.- Trainer/in: Sergej-Alexander Breiter
- Trainer/in: Karl Fürlinger
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.
- Trainer/in: Maximilian Höb
- Trainer/in: Dieter Kranzlmüller