Teaching

Lectures

In the summer semester 2024, I was the lecturer for the course Cyber-Physical Systems II: Program Verification. SS24

In this course, designed in 2019 by Matthias Heizmann, Tanja Schindler and me, we develop the syntax and formal semantics of a simple imperative programming language. We use this language to introduce students to a variety of different approaches to program verification, from Hoare logic, over predicate transformers and symbolic execution, abstract interpretation (*new in 2024*), all the way to CEGAR-based verification algorithms such as predicate abstraction and trace abstraction.

15 students attended this elective course and participated in the oral exams. In a ranking calculated by the dean of studies based on anonymous student evaluation forms, the course was ranked first among all computer science courses offered at the Technical Faculty in this semester.

I also co-organise several lectures offered by the Chair for Software Engineering.

• Cyber-Physical Systems I: Discrete Models WS23/24 WS22/23 WS21/22 WS20/21 WS19/20

  This lecture is based on the book Principles of Model Checking by Baier and Katoen, and introduces students to formal modeling of cyber-physical, reactive systems as transition systems. We discuss different modeling formalisms, specifications in the form of linear-time properties, and the automata-theoretic approach to linear-time (LTL) model checking.

• Cyber-Physical Systems II: Program Verification SS22 SS21 SS20 SS19

  In this lecture, we develop the syntax and formal semantics of a simple imperative programming language. We use this language to introduce students to a variety of different approaches to program verification, from Hoare logic, over predicate transformers and symbolic execution, all the way to CEGAR-based verification algorithms such as predicate abstraction and trace abstraction.

• Theoretical Computer Science (dt: Theoretische Informatik) SS23 SS22

  This course introduces students to the foundations of computation. It covers formal languages, grammars, the Chomsky hierarchy, automata theory, Turing machines, decidability and complexity theory.

Seminars

I frequently supervise students in the different seminars offered by the Chair for Software Engineering.

• Classical Articles of Program Analysis (dt: Klassische Artikel der Programmanalyse, BSc Proseminar) WS21/22 WS20/21 WS19/20
• Automata Theory (dt: Automatentheorie, BSc Proseminar / Seminar) WS22/23 SS21 SS20
• Advanced Topics in Program Analysis (MSc seminar) WS20/21

In our seminars, students are given source material on their assigned topic (either a research paper, or a book chapter). The students then write a proposal, describing their plan for a 25min research talk on the topic. Students typically review one or more proposals by other students. The talks are either given throughout the semester, or as a “block seminar” in 1-2 days near the end of the semester.

Student Projects

I have supervised a number of student projects revolving around program analysis and automata theory. Such projects typically involve a theoretical component (e.g. design / modification and correctness proof of some algorithm) and an implementation and evaluation component in the context of the program analysis and automata theory framework Ultimate.

If you are interested in a project or thesis, send me an email. You can find a list of possible topic areas in the Ultimate wiki.

• Combination Operators for Monitor-Based Preference Orders BSc Projectongoing
• Computing omega-Reductions with Ample Sets MSc Projectongoing
• Translating YAML correctness witnesses for deductive verifiers BSc Thesisongoing
• Constructing Empire Annotations from Petri Nets BSc Thesis2024
• Büchi-Mealy Contraction and the Maximal Cut Property BSc Thesis2024
• Detection and Integration of Conditional Commutativity for Concurrent Program Verification MSc Thesis2024
• Computing Small Proofs for Concurrent Programs BSc Project2024
• Stratified Source Sets BSc Project2023
• Selecting Preference Orders MSc Project2023
• Stratified Reduction with Dynamic Abstractions BSc Thesis2023
• Dynamic Partial Order Reduction on Tree-shaped Automata for Verification of Concurrent Programs BSc Thesis2023
• Computing Representative Automata for Maximal Causality Reduction MSc Thesis2022
• Statement Abstraction for POR MEd Project2022
• Owicki-Gries Correctness Proofs from Petri Net Unfoldings MSc Thesis2021
• Trace Abstraction Refinement with Repeated Lipton Reduction MSc Project2021
• Tight integration of Partial Order Reduction into Trace Abstraction Refinement BSc Thesis2021
• Owicki-Gries Correctness Proof Scheme MSc Project2021
• Clinical Guidelines Verification with ULTIMATE: A Case-Study Approach MSc Thesis2020
• Trace Abstraction with Maximal Causality Reduction MSc Thesis2020
• Large Block Encoding for Concurrent Programs BSc Thesis2019