Teaching

WS 2011/2012

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

• Core lecture course: Verification. How can on ensure that computer programs actually do what they are intended to do? Simply testing the program on a few inputs is insufficient to prove the absence of bugs. In this lecture course, we will take a look at automated methods to verify the functional correctness of systems. The goal of these methods is to deliver a formal proof of correctness for a given system. We will cover the theory and practice of both deductive methods for program verification and state space exploration methods like model checking for concurrent programs.

SS 2011

• 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: Games, Synthesis and Robotics. In this seminar, we will explore the theory and applications of infinite games. In particular, we consider the automatic synthesis of control software for robots. We offer seminar topics broadly classifiable into two categories: Foundational aspects, i.e. game solving, variants of synthesis and temporal logic and applied aspects, i.e. robotic control software in combination with our hardware platform, three e-puck robots.

WS 2010/2011

• Core lecture course: 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.

SS 2010

• Grundlagenvorlesung: 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.

WS 2009/2010

• Core lecture course: 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.

WS 2008/2009

• Core lecture course: 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, autos), telecommunication equipment (e.g., mobile phones), and consumer eletronics 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.

SS 2008

• Advanced course: 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: Games in Verification and Synthesis. In this seminar, we will study game-theoretic methods that derive implementations from formal specifications (synthesis) and that prove that a given implementation satisfies a logical property (verification). In both cases, we view the interaction between a software component and its environment as an infinite game; verification then amounts to checking that the strategy represented by the program is winning; synthesis amounts to deriving a winning strategy from a logical description of the winning condition.

WS 2007/2008

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

SS 2007

• 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 of the information processing in transportation systems (e.g., airplanes, trains, autos), 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.

WS 2006/2007

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

SS 06

• Decision Procedures for Verification. Decision procedures for the satisfiability of logical formulas in first-order theories. Decision procedures for propositional logic. Decision procedures for the theories of equality, real numbers, integer numbers, lists, arrays, sets, and multisets. Cooperation methods: integration, combination, reduction.

• The Time Machine. Proseminar. Blockveranstaltung nach Semesterende.

WS 2005/2006

• Lab Course Verification. In this lab course we apply computer-aided verification tools to obtain a mathematical proof that an entire computer system is correct. Our target application is a simple communication tool, which we analyze across all system layers, including the hardware and the operating system. For this task we apply a range of state-of-the-art verification tools, including computer-aided theorem provers (ISABELLE) and model checkers (SMV,SPIN).

SS 05

• Programmierung II. Die Vorlesung Programmierung II richtet sich an Studierende im Grundstudium. In den ersten Vorlesungswochen werden Grundkenntnisse der objektorientierten Programmierung und der Programmiersprache C++ vermittelt. Im Theorieteil der Vorlesung diskutieren wir effiziente Datenstrukturen (Listen, Arrays, Bäume, Graphen, Hashing, usw.) und wichtige Algorithmen, in denen diese Datenstrukturen Anwendung finden.

WS 04/05

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

SS 04

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

WS 03/04

• Programming Languages. Programming languages provide the abstractions, organizing principles, and control structures that programmers use to write good programs. In this course we study the concepts that appear in programming languages, issues and trade-offs that arise in their design, and the way that language design affects program development.

SS 03

• Verification The cause of the catastrophic crash of the Ariane 5 rocket in 1996 was traced to a simple problem in the computer software that calculated the rocket’s position. Despite rigorous testing of the software, the problem went unnoticed. Such software failures occur every day—-though usually with less spectacular consequences. 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. In the early years of verification research, the focus was on deductive proof systems. Back then, program verification was mostly done manually. 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. Verification research continues actively in both academia and industry (see conferences like CAV and TACAS, and verification projects by IBM, Microsoft, Bell Labs and many others).

WS 02/03

• Automata, Games & Verification. Infinite games and automata on infinite objects as foundations for the automated verification of reactive systems.