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.

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.

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)