- Trainer/in: Evi Berchtold
- Trainer/in: Armin Hadziahmetovic
- Trainer/in: Markus Joppich
- Trainer/in: Samuel Klein
- Trainer/in: Felix Offensperger
- Trainer/in: Ralf Zimmer
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, 10:15-11:45
- Location: Seminar Room 133, Oettingenstr. 67
- First meeting: 2024-04-18 (about the detailed seminar organization and expectations)
Content
Model checking is an important research field in computer science where automatic solutions to the following problem are studied: Given a computational model and a specification, decide whether the model satisfies the specification or not. In practice, a computational 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 model. Compared to testing, model checking can guarantee the correctness of a computational model 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:
- Reading sessions: 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.
- Weekly 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.
- 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
- Trainer/in: Dirk Beyer
- Trainer/in: Po-Chun Chien
- Trainer/in: Niann-Tzer Li
Any questions please email to yunru.wang@ifi.lmu.de
Time & Location：
Thursdays 16:00-18:00, Room U 133, Oettingenstr. 67
Introduction：
Code semantics form the backbone of numerous program analysis tasks, such as software testing, vulnerability detection, and reverse engineering. In recent years, we have witnessed an initial surge in applying ML to facilitate the understanding of code semantics and further enhance downstream analysis tasks. Unlike traditional methods, ML in program analysis needs less expert knowledge, offering promising accuracy and efficiency. However, challenges remain. To take binary code as illustration, how to ensure generalization and scalability across diverse platforms, compilers, optimization options and obfuscation are still open questions. Additionally, the reliability and usage boundaries of ML in program analysis prompt ongoing discussions.In this seminar, we will delve into the development of ML techniques for code semantic representation. Tracing its evolution from applying traditional ML algorithms to large language models, as well as the shift from manual feature engineering to self-supervised tasks and neural networks specifically designed for code semantics.
This seminar aims to deepen your understanding of code semantics and neural networks through discussions and coding practices.
Pre-requisites：
- in English
- Attendance at the first session (18-04-2024) is mandatory.
- Interest in binary analysis and a basic knowledge of machine learning.
- Trainer/in: Johannes Kinder
- Trainer/in: Yunru Wang
This
seminar offers a variety of topics from High Performance Computing,
Quantum Computing, Virtual Reality and Cryptography for students to work
on.
Each participant will
work on one topic throughout the semester (master students on their
own, bachelor students in pairs). The goal is to write a paper, submit
it to an imaginary conference committee, review each other's work and
present their findings at an end-of-term "conference" in the seminar.
The task is supported by a lecture about scientific writing and presentations and by an individual supervisor for each topic.
The mandatory lectures will take place on Wednesdays, 12-14 h c.t., room 061 in Oettingenstr. 67.
The exam date will likely be a Saturday in July (update expected soon).
- Trainer/in: Karl Fürlinger
- Trainer/in: Sophia Grundner-Culemann
- Trainer/in: David Linder
Dependent type theories are formal systems which can be understood both as powerful logics and functional programming languages. They have been studied since the late 1960’s and today serve as the foundations of popular interactive theorem provers such as Agda, Coq, Idris and Lean. In this seminar, we will discuss various important type theories and their properties.
You can register for this seminar only via the central allocation of MSc seminars.
- Trainer/in: Jasmin Blanchette
- Trainer/in: Jannis Limperg
This seminar covers recent topics and advances in Reverse Engineering techniques aided by Machine Learning. We will cover recovery of function boundaries, symbols, and in particular Deep Learning models that produce vector representations of machine code.
Participants should have basic knowledge in Machine Learning and should be somewhat familiar with assembly code.
Participation in the first session (April 17) is mandatory, anyone not present (without valid excuse) cannot take this seminar. Seminar sessions take place Wednesdays 4pm-6pm at Oettingenstr. 67, room 033 from 17.4.-17.7.24
After the first session, the participants will choose their paper. The first presentations start two weeks after. Each participant is required to give a presentation of his paper, prepare a discussion, participate in every week's discussion, and write a seminar report at the end of the term.
- Trainer/in: Moritz Dannehl
- Trainer/in: Johannes Kinder
- Trainer/in: Ruotong Liao
- Trainer/in: Volker Tresp
- Trainer/in: Jingpei Wu
- Trainer/in: Dirk Beyer
- Trainer/in: Marvin Brieger
- Trainer/in: Marian Lingsch Rosenfeld
- Trainer/in: Eyke Hüllermeier
- Trainer/in: Alireza Javanmardi
- Trainer/in: Timo Löhr
Im Rahmen dieses Seminars werden ausgewählte Themen aus dem Bereich der Mobilen und Verteilten Systeme behandelt, die insbesondere aus den Forschungsschwerpunkten des Lehrstuhls stammen. In den letzten Semestern führte das zu einem Fokus auf Themen aus dem Bereich des Maschinellen Lernens und Quantum Computing.
- Trainer/in: Maximilian Mansky
- Trainer/in: Leo Sünkel
- Trainer/in: Maximilian Zorn