- 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.