Teaching

Winter 2024/2025

Advanced lecture: Automata, Games and Verification
The theory of automata over infinite objects provides a succinct, expressive, and formal framework for reasoning about reactive systems, such as communication protocols and control systems. Reactive systems are characterized by their nonterminating behaviour and persistent interaction with their environment. In this course we will study the main ingredients of this elegant theory, and its application to automatic verification (model checking) and program synthesis.

Summer 2024

Seminar: Neural-Symbolic Computing
The way our brain forms thoughts can be classified into two categories (according to Kahneman in his book “Thinking Fast and Slow”):
System 1: fast, automatic, frequent, stereotypic, unconscious (e.g. “Is this a cat or a dog?” or “What does this sentence mean in English?”) and
System 2: slow, effortful, logical, conscious (e.g. “17*16 = ?” or “If a → b does b → a?”).
The traditional view is that deep learning is limited to System 1 type of reasoning. Mostly because of the perception that deep neural networks are unable to solve complex logical reasoning tasks reliably. Historically, applications of machine learning were thus often restricted to sub-problems within larger logical frameworks, such as resolving heuristics in solvers.
In this seminar, we will explore new research that shows that deep neural networks are, in fact, able to reason on “symbolic systems”, i.e., systems that are built with symbols like programming languages or formal logics.

Winter 2023/2024

Core Lecture: Verification
Computers and programs are everywhere, including in critical places where human lives are at stake (airplanes, hospitals, nuclear power plants, …). In this context, how can one ensure that computer programs do what they are intended to do without harming humans? To answer this question, one could stress-test the robustness of programs by running them repeatedly with various inputs to identify which might cause a failure. This solution is unsatisfactory because the input spaces can be unreasonably large, and testing all scenarios is simply out of reach. It is possible to tailor a tester to test a given program, but present-day programs are so complex that traditional testing techniques can leave significant bugs undetected. Another approach is to prove, once and for all, that programs are correct using mathematical and logical methods. This approach was pioneered by, among others, Dijkstra, Floyd, Gries, Hoare, Lamport, Manna, Owicki, and Pnueli. Their research led to the development of an extensive array of techniques to establish, formally, the conformance of programs to a given specification. Today, these techniques have evolved into powerful verification tools that can automatically prove the correctness of large programs. Model Checking is one of these “push-button” verification technologies. Given a program and a specification, a model checker can automatically verify that the program is correct or identify a scenario where it fails to satisfy its specification. This course takes an up-to-date look at the theory and practice of program verification using model-checking methods. This approach was pioneered by, among others, Dijkstra, Floyd, Gries, Hoare, Lamport, Manna, Owicki and Pnueli. Today, we have powerful decision procedures that can, completely automatically, answer basic questions about the data types typically used by programmers. Model Checking is a “push-button” technology that can analyze finite-state abstractions of programs with as many as 10²⁰ states. This course takes an up-to-date look at the theory and practice of program verification.

Summer 2023

Seminar: Hyperproperties.
Traditional specification languages for systems usually refer to single execution traces and are therefore insufficient in many security-critical applications. This is because attackers may use comparisons between several different system traces to infer hidden secrets. Hyperproperties address this problem: Instead of specifying permitted behavior on single traces, they do so for sets of traces. The importance of research on hyperproperty specification and verification methods has recently been demonstrated by high-profile attacks such as Spectre and Meltdown, which exploit systems that violate certain information-flow policies. Further details on these attacks and their relation to hyperproperties can be found in this blog post.

Winter 2022/2023

Advanced lecture: Automata, Games and Verification
The theory of automata over infinite objects provides a succinct, expressive, and formal framework for reasoning about reactive systems, such as communication protocols and control systems. Reactive systems are characterized by their nonterminating behaviour and persistent interaction with their environment. In this course we will study the main ingredients of this elegant theory, and its application to automatic verification (model checking) and program synthesis.

Summer 2022

Proseminar: From Program Verification to Synthesis
Proving that a program is correct is hard. Generating a correct-by-construction program is even harder. In this proseminar we cover a foundational approach to these problems, based on automata theory. We study different algorithms for program verification and synthesis, with respect to different specifications (such as LTL and HyperLTL), as well as a compositional approach for both verification and synthesis problems.

Seminar: Neural-Symbolic Computing
The way our brain forms thoughts can be classified into two categories (according to Kahneman in his book “Thinking Fast and Slow”):
System 1: fast, automatic, frequent, stereotypic, unconscious (e.g. “Is this a cat or a dog?” or “What does this sentence mean in English?”) and
System 2: slow, effortful, logical, conscious (e.g. “17*16 = ?” or “If a → b does b → a?”).
The traditional view is that deep learning is limited to System 1 type of reasoning. Mostly because of the perception that deep neural networks are unable to solve complex logical reasoning tasks reliably. Historically, applications of machine learning were thus often restricted to sub-problems within larger logical frameworks, such as resolving heuristics in solvers.
In this seminar, we will explore new research that shows that deep neural networks are, in fact, able to reason on “symbolic systems”, i.e., systems that are built with symbols like programming languages or formal logics.

Winter 2021/2022

Core Lecture: Verification.
How can one ensure that computer programs actually do what they are intended to do? Simply running a program repeatedly with various inputs is inadequate, because one cannot tell which inputs might cause the program to fail. It is possible to tailor a tester to test a given program, but present-day programs are so complex that they cannot be adequately checked through conventional testing, which can leave significant bugs undetected. Program verification uses mathematical and logical methods to prove that a program is correct. This approach was pioneered by, among others, Dijkstra, Floyd, Gries, Hoare, Lamport, Manna, Owicki and Pnueli. Today, we have powerful decision procedures that can, completely automatically, answer basic questions about the data types typically used by programmers. Model Checking is a “push-button” technology that can analyze finite-state abstractions of programs with as many as 10²⁰ states. This course takes an up-to-date look at the theory and practice of program verification.

Summer 2021

Seminar: Monitoring of Cyber-Physical Systems.
A cyber-physical system is a digital component that controls a physical object such as an autonomous car, a nuclear power plant, or a medical implant. Cyber-physical systems are hard to design correctly; they are also difficult to test or verify. In this seminar, we will study dynamic analysis methods, where a monitoring component observes the behavior of the system and determines whether it is in a safe or unsafe state. If a problem is detected, the monitor raises an alarm and prompts the system to initiate a mitigation protocol. We will take a look at state-of-the-art runtime monitoring techniques for cyber-physical systems and discuss recent developments in this field.

Proseminar: Software Reliability.
Software is used in more and more applications where errors seriously affect the safety and/or security of the system. How can we ensure that the programs work as intended? In this proseminar, we will study a broad spectrum of techniques that increase the quality of software through the use of formal methods. We will discuss and compare formal software models, process algebras, specification techniques, and techniques for automated testing and automatic verification.

Winter 2020/2021

Grundvorlesung: Programmierung 1.
Was ist Informatik? Was ist Programmieren? Dieser Kurs bietet eine Einführung in die grundlegenden Konzepte der Informatik und insbesondere der Programmiersprachen. Wir verwenden bewusst die funktionale Programmiersprache Standard ML, da sie die Konzepte der Informatik, insbesondere die Rekursion, einfach und klar umsetzen lässt. Der Fokus der Vorlesung liegt auf der Struktur von Programmiersprachen, welche durch Grammatiken, Inferenzregeln, und das Programmieren von Interpretern, Maschinen und Übersetzern vermittelt wird. Darauf aufbauend werden wir grundlegende Techniken wie Laufzeitbestimmungen und (Korrektheits-)Beweise über Programme behandeln.
Am Ende der Vorlesung werden Sie in der Lage sein eigene Programmiersprachen zu definieren und Interpreter dafür zu schreiben.

Summer 2020

Seminar: Neural-Symbolic Computing.
The way our brain forms thoughts can be classified into two categories (according to Kahneman in his book “Thinking Fast and Slow”):
System 1: fast, automatic, frequent, stereotypic, unconscious (e.g., “Is this a cat or a dog?” or “What does this sentence mean in English?”) and
System 2: slow, effortful, logical, conscious (e.g., “17*16 = ?” or “If a → b does b → a?”).
The traditional view is that deep learning is limited to System 1 type of reasoning. Mostly because of the perception that deep neural networks are unable to solve complex logical reasoning tasks reliably. Historically, applications of machine learning were thus often restricted to sub-problems within larger logical frameworks, such as resolving heuristics in solvers.
In this seminar, we will explore new research that shows that deep neural networks are, in fact, able to reason on “symbolic systems”, i.e., systems that are built with symbols like programming languages or formal logics.

Winter 2019/2020

Advanced Lecture: Reactive Synthesis.
Many of today’s problems in computer science are no longer concerned with programs that transform data and then terminate, but with non-terminating systems that are in constant interaction with their (possibly antagonistic) environment. Over the course of the last fifty years it turned out to be very fruitful to model and analyze such reactive systems in a game-theoretic framework, which captures the antagonistic and strategic nature of the interaction between the system and its environment. Despite the prohibitive complexity of these problems in general, in recent years it has been shown that many benchmark problems can be solved automatically by efficient implementations of game-solving algorithms.
In this lecture, we will introduce different types of two-player games of infinite duration, and algorithms to solve them. To obtain efficient implementations, we will also cover automated reasoning methods that can be used as subprocedures in a synthesis algorithm, as well as data structures that can efficiently represent important aspects of infinite games.
During the course, students will implement a synthesis tool using their knowledge acquired during the lecture. At the end of the course, the resulting tools will be compared against each other and state-of-the-art tools on a set of benchmarks from the official Reactive Synthesis Competition.

Core Lecture: Verification.
How can one ensure that computer programs actually do what they are intended to do? Simply running a program repeatedly with various inputs is inadequate, because one cannot tell which inputs might cause the program to fail. It is possible to tailor a tester to test a given program, but present-day programs are so complex that they cannot be adequately checked through conventional testing, which can leave significant bugs undetected. Program verification uses mathematical and logical methods to prove that a program is correct. This approach was pioneered by, among others, Dijkstra, Floyd, Gries, Hoare, Lamport, Manna, Owicki and Pnueli. Today, we have powerful decision procedures that can, completely automatically, answer basic questions about the data types typically used by programmers. Model Checking is a “push-button” technology that can analyze finite-state abstractions of programs with as many as 10²⁰ states. This course takes an up-to-date look at the theory and practice of program verification.

Summer 2019

Block Seminar: Hybrid Systems.
The interaction of a computer system with physical processes is a clash of two worlds: a computer works in a clocked, discrete world with clear semantics. When the processor’s edge rises, the internal state changes, when it falls, the world stands still. The real, physical world, however, is chaotic: nature does not wait for a clock tick to apply changes. Yet, the interaction of machines with the real world is essential. Machines control power plants, cars, satellites and factories. Such systems are called “Hybrid Systems”, a mixture of continuous, physical processes and discrete, logical steps. In this seminar we will cover an interesting range of topics concerning hybrid systems such as analysis methods, synthesis and runtime monitoring.

Proseminar: Softwarezuverlässigkeit.
Wie kann sichergestellt werden, dass Software zuverlässig funktioniert? Durch die steigende Komplexität von Software wird es für Entwickler immer schwieriger, diese vollständig zu überblicken und ihre Korrektheit zu garantieren. In diesem Proseminar beschäftigen wir uns mit formalen Methoden zur Sicherstellung von Softwarezuverlässigkeit.

Winter 2018/2019

Advanced lecture: Automata, Games and Verification.
The theory of automata over infinite objects provides a succinct, expressive and formal framework for reasoning about reactive systems, such as communication protocols and control systems. Reactive systems are characterized by their nonterminating behaviour and persistent interaction with their environment. In this course we study the main ingredients of this elegant theory, and its application to automatic verification (model checking) and program synthesis.

Seminar: Hyperproperties.
Traditionally, when speaking about properties of a system, we mean properties which refer to a single execution trace of the system. However, trace properties have limited expressivity as they do not allow us to compare several possible execution traces. Hyperproperties address this problem: Instead of referring to a single trace, they refer to sets of traces. In this seminar, we will have a look at state-of-the-art research on hyperproperties. This ranges from research on logics that describe hyperproperties, over algorithms that check (statically or at run-time) whether a system fulfils a property, to practical applications of this research in domains such as conference-management systems.

Summer 2018

Proseminar: Formal Verification of Security Protocols.
Security protocols are omnipresent in our daily lives in areas such as online banking and mobile phones. Their purpose is to keep our transactions and personal data secure. Because these protocols are implemented on potentially insecure networks like the internet, they are notoriously difficult to devise. The field of formal analysis of security protocols has seen significant advances during the last years. There is now a better understanding of decidability and complexity questions, and models with solid theoretical foundations have been developed together with proof techniques. Automated tools based on these insights have been designed and successfully applied to numerous protocols, including industrial protocols. In this Proseminar, we will look at the recent and ongoing work in this very active field of research.

Core Lecture: Embedded Systems.
When asked about computers and processors most people immediately imagine a laptop or a PC sitting under a desk. In reality, however, only a small fraction of processors are actually used for such systems. The major part is used as embedded components in larger systems, often not directly visible to the user.
They control everyday devices such as TVs, microwaves, and alarm clocks, but also highly safety-critical systems like air control, nuclear reactor control, automatic defibrillators, and robotic surgery-assistance systems.
Embedded systems often interact with the real world. An automatic thermostat gets information about the environment by sensing the room temperature and actively changes the environment by turning on the heater. This introduces several new challenges such as real-time dependent control and noise in input data.
In this course, we will have a closer look at the theoretical and practical aspects of designing reliable embedded systems. The theoretical foundations studied in this course are complemented by a practical project. Here, participants can immediately experience and overcome emerging problems discussed in theory.

Winter 2017/2018

Grundvorlesung: Programmierung 1.
Was ist Informatik? Was ist Programmieren? Dieser Kurs bietet eine Einführung in die grundlegenden Konzepte der Informatik und insbesondere der Programmiersprachen. Wir verwenden bewusst die funktionale Programmiersprache Standard ML, da sie die Konzepte der Informatik, insbesondere die Rekursion, einfach und klar umsetzen lässt. Der Fokus der Vorlesung liegt auf der Struktur von Programmiersprachen, welche durch Grammatiken, Inferenzregeln, und das Programmieren von Interpretern, Maschinen und Übersetzern vermittelt wird. Darauf aufbauend werden wir grundlegende Techniken wie Laufzeitbestimmungen und (Korrektheits-)Beweise über Programme behandeln.
Am Ende der Vorlesung werden Sie in der Lage sein eigene Programmiersprachen zu definieren und Interpreter dafür zu schreiben.

Advanced Lecture: Reactive Synthesis.
Many of today’s problems in computer science are no longer concerned with programs that transform data and then terminate, but with non-terminating systems that are in constant interaction with their (possibly antagonistic) environment. Over the course of the last fifty years it turned out to be very fruitful to model and analyze such reactive systems in a game-theoretic framework, which captures the antagonistic and strategic nature of the interaction between the system and its environment. Despite the prohibitive complexity of these problems in general, in recent years it has been shown that many benchmark problems can be solved automatically by efficient implementations of game-solving algorithms.
In this lecture, we will introduce different types of two-player games of infinite duration, and algorithms to solve them. To obtain efficient implementations, we will also cover automated reasoning methods that can be used as subprocedures in a synthesis algorithm, as well as data structures that can efficiently represent important aspects of infinite games.
During the course, students will implement a synthesis tool using their knowledge acquired during the lecture. At the end of the course, the resulting tools will be compared against each other and state-of-the-art tools on a set of benchmarks from the official Reactive Synthesis Competition.

Proseminar: Time Machine.
This Proseminar is designed to teach how to give a scientific presentation. Students will read up on a topic, summarize it, and teach the findings to their fellows in a presentation. After a practice run, students are asked to give feedback, enabling a process of improvement for the final presentation.
All topics are concerned with time, aiming to answer the fundamental questions of how to specify temporal properties, model temporal systems, and decide satisfaction of temporal properties in a temporal system.
Literature is only available in English, and we encourage presentations in English. Nevertheless, German is allowed, too.

Winter 2016/2017

Seminar: Runtime Verification
Runtime verification is a dynamic analysis method, where an execution of a system is checked during runtime against a specification. Runtime verification serves as a supplement to traditional verification methods, such as model checking and testing, and can be used prior to deployment for analysis and debugging purposes. The major advantage of runtime verification, however, emerges in the role it plays after deployment, for ensuring reliability, safety, and security and for providing fault containment and recovery as well as online system repair.

Core Lecture: Verification
How can one ensure that computer programs actually do what they are intended to do? Simply running a program repeatedly with various inputs is inadequate, because one cannot tell which inputs might cause the program to fail. It is possible to tailor a tester to test a given program, but present-day programs are so complex that they cannot be adequately checked through conventional testing, which can leave significant bugs undetected. Program verification uses mathematical and logical methods to prove that a program is correct. This approach was pioneered by, among others, Dijkstra, Floyd, Gries, Hoare, Lamport, Manna, Owicki and Pnueli. Today, we have powerful decision procedures that can, completely automatically, answer basic questions about the data types typically used by programmers. Model Checking is a “push-button” technology that can analyze finite-state abstractions of programs with as many as 10²⁰ states. This course takes an up-to-date look at the theory and practice of program verification.

Summer 2016

Core Lecture: Embedded Systems.
Embedded systems are computer systems that are encapsulated into larger products, and that are normally not directly visible to the user. Embedded systems are responsible for the information processing in transportation systems (e.g., airplanes, trains, cars), telecommunication equipment (e.g., mobile phones), and consumer electronics products (e.g., TVs, DVD-players).
In this course we will study the theoretical foundations and practical tools that are needed to build reliable and efficient embedded systems. An important component of the course is the project, where groups of participants design and build an embedded system.

Advanced Lecture: Infinite Games.
Many of todays problems in computer science are no longer concerned with programs that transform data and then terminate, but with non-terminating systems which have to interact with a possibly antagonistic environment. The emergence of so-called “reactive systems” requires new approaches to verification and synthesis. Over the course of the last fifty years it turned out to be very fruitful to model and analyze reactive systems in a game-theoretic framework, which captures the antagonistic and strategic nature of the interaction between the system and its environment.
In this lecture, we will study different types of two-player games of infinite duration: typical questions we will answer are “how hard is it to determine the winner of a given game?”, “what kind of strategy does the winner need to win the game?”, and “does every game have a winner?”. Also, we discuss applications of infinite games in logics by proving Rabin’s theorem, sometimes called the “mother of all decidability results”.

Winter 2015/2016

Grundvorlesung: Einführung in eingebettete Systeme.
Insulinpumpen, Spülmaschinen, DVD-Recorder, Solaranlagen, Hochgeschwindigkeitszüge und moderne Nähmaschinen haben alle etwas gemeinsam: Sie funktionieren, weil einer oder gar mehrere Computer in ihnen rechnen. Die Vorlesung gibt eine Einführung in die Modellierung, das Design und die Analyse solcher eingebetteter Systeme.

Seminar: Trends in Software Synthesis.
Program synthesis in its classical formulation is concerned about finding a program that meets a specification given as a logical formula. Recent work on program verification and program optimization have shown potential benefits of allowing the user to supplement the logical specification with a syntactic template that constrains the space of allowed implementations.
In this seminar we look into various novel approaches in program synthesis. The topics will be divided mainly into three categories. Deductive Synthesis, where synthesis is regarded as a theorem proving task, syntax-guided synthesis, where a partial program with incomplete information is completed using user-specified assertions and finally, learning-based approaches, where the synthesis procedure is formulated as a learning algorithm between an oracle and the synthesizer.
The seminar is split into two parts. The first part will take the form of reading sessions, where we lay the foundations of the topic. The second part will consist of presentations about recent papers from the three categories mentioned above.

Summer 2015

Doctoral privatissimum: Hyperproperties.
Trace properties, i.e., sets of execution traces, have long been used to specify the correctness of computer systems. There are, however, important properties that are impossible to describe by referring to individual execution traces. Information flow policies, which characterize the circumstances under which an external observer can distinguish two executions, are of this type. Other examples include symmetric access to a shared resource, and the correctness of encoders and decoders for error resistant codes. Because these properties are properties of sets of execution traces, rather than properties of individual traces, they are called hyperproperties. In this doctoral privatissimum, we will survey and criticize different ways to specify and verify hyperproperties.

Advanced lecture: Automata, Games and Verification.
The theory of automata over infinite objects provides a succinct, expressive and formal framework for reasoning about reactive systems, such as communication protocols and control systems. Reactive systems are characterized by their nonterminating behaviour and persistent interaction with their environment. In this course we study the main ingredients of this elegant theory, and its application to automatic verification (model checking) and program synthesis.

Proseminar: Softwarezuverlässigkeit.
In diesem Proseminar geben wir einen Überblick zu Methoden zur Verbesserung von Softwarezuverlässigkeit. Beginnend bei Verfahren wie automatisiertem Testen, besprechen wir dann formale Softwaremodelle, Prozessalgebren und Spezifikationen bis hin zu automatischer Softwareverifikation. Ein Fokus liegt auch auf dem Erlernen wissenschaftlichen Arbeitens.

Advanced lecture: Recursion Theory.
Recursion Theory, also known as Computability Theory, is the study of the foundations of computation. Typical questions we will study are “Which functions can be computed?”, “How can the notion of algorithm be formalized and are those formalizations equally expressive?”, and “Are some non-computable problems harder than others?”.
We will answer these questions by studying a simple programming language and a mathematical model of computation, and by proving their equivalence, thereby answering the first two questions. Then, we delve into the theory of non-computable functions to answer the third question.
Recursion theory stands out as a beautiful theory with oftentimes simple, short, and surprising proofs and historically forms the basis of complexity theory.