- 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 todays 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.
- 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 1020 states. This course takes an up-to-date look at the theory and practice of program verification.
- 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”.
- 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.
- 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.
- Core lecture (offered in block form after lecture period): Verification.
- Advanced Lecture: Automata, Games & Verification.