Teaching

This page summarizes all courses that I am currently teaching or have been teaching in the past.

Current Courses

Fall 2023

02245 Program Verification

Regular Courses

I am teaching the following courses at DTU every year:

02245 Program Verification (7.5 ECTS at MSc level)

This course offers a hands-on introduction to the usage, construction, and theory of automated deductive program verifiers. In particular, it introduces

1. program logics for writing formal correctness proofs (for example weakest preconditions and separation logic);

2. SMT solvers (for example Z3) for automating reasoning about logical formulas;

3. intermediate verification languages (for example Viper) for encoding verification methodologies; and

4. source code verifiers for handling feature-rich programming languages.

The course will intermix technical content with hands-on experience. Students should acquire the skills to apply and extend tool-supported methodologies for developing proven-correct software.

• DTU course database

• Read more

02141 Computer Science Modelling (10 ECTS at BSc level)

The courses introduces central models and formalisms from computer science. Students will develop tools based on these formalisms, and use those tools to run and analyse software code.

The course covers two main topics:

1. Formal languages and their use for describing syntax and computations. For regular languages we consider ways to describe them with finite automata and regular expressions, relations between those, practical applications (e.g. searching in texts, lexical analysis, formal specifications) and some key theoretical properties (e.g. decidability of fundamental problems). For context free languages we consider ways of describing them with context-free grammars and pushdown automata, their relation, and practical applications (e.g. parsing programs, documents and formatted data).

2. Formal Methods and their use for both modelling and analysis of properties of IT systems, in particular software code. This includes semantics of programming languages, program interpretation, program verification, program analysis, security analysis and model checking.

The course includes hands-on experience with various tools, and the students are asked to solve theoretical as well as practical exercises, which integrate the two topics of the course.

• DTU course database

Past Courses

I have been teaching the following courses and supervised students in the following seminars (at DTU if no other indication is provided):

Spring 2023	02141 Computer Science Modelling (together with Alberto Lluch Lafuente)
	02913 Advanced Analysis Techniques (together with Andrey Rivkin)
Fall 2022	Rust Programming Concepts (3-week course)
	02245 Program Verification
Spring 2022	02141 Computer Science Modelling (together with Alberto Lluch Lafuente)
Fall 2021	Guest lecture on “Ownership and Lightweight Automated Verification” in Flemming Nielson’s program analysis course
Spring 2021	Program Verification (at ETH Zürich, together with Peter Müller)
Summer 2018	Static Methods for Quantitative Program Analysis (Seminar at RWTH Aachen)
	Formal Verification Meets Machine Learning (Seminar at RWTH Aachen)
Winter 2017	Foundations of Probabilistic Programming (Seminar at RWTH Aachen)
Winter 2016	Analysis and Verification of Pointer Programs (Seminar at RWTH Aachen)
Summer 2016	Probabilistic Programming (Seminar at RWTH Aachen)
	Theoretical Foundations of Programming Languages (Seminar at RWTH Aachen)
Summer 2015	Principles of Programming Languages (Seminar at RWTH Aachen)