Selected Topics Design and Verification

Course Number 705070 | Sommersemester 2020


In this course, you will learn about cutting edge advancements in the field of Design and Verification of software and hardware systems from a formal perspective. Typically, we start by presenting the preliminaries on formal languages and formal methods. Having covered basic concepts on formal methods and advancements in automata theory, we study how these concepts are applied to design and verification of hardware and software systems.

We update the content of this course on an annual basis. This year’s topic is reactive synthesis.

The lecture notes are available as PDF documents and show one slide per page.

New: Every Wednesday, we have a question hour from 12pm-1pm.

Number Date Lecturer Topic Slides Videos
1 2020-03-10 Roderick Bloem Introduction slides intro
2 2020-03-17 Vedad Hadzic Introduction SMT (Z3) Introduction-to-SMT-with-Z3.pdf Video Intro SMT
3 2020-03-24 Bettina Könighofer Bounded Synthesis, safety only slides_bounded_synthesis_safety Video Bounded Synthesis Safety
4 2020-03-31 Masoud Ebrahimi LTL Lecture Part1Part2
5 2020-04-21 Roderick Bloem SMT – Theory slides_smt_theory Part1, Part2
6 2020-04-28 All SCOS members Presentations Exercise 1 by Students
7 2020-05-05 Benedikt Marderbacher Omega Automata slides_omega_automata video_omega_automata
8 2020-05-12 Benedikt Marderbacher Bounded Synthesis slides_bounded_synthesis video_bounded_synthesis
9 2020-05-19 Bettina Könighofer Synthesis via Games, Games 1 slides_games1
10 2020-05-26 Bettina Könighofer Synthesis via Games, Games 2
11 2020-06-09 Bettina Könighofer Relation Determinization slides_relation_determinization
12 2020-06-16 All SCoS Members Research
13 2020-06-23 All SCoS Members Presentations Exercise 2 by Students


You find here the homework for the course.

Number Due Date Topic Slides
1 2020-03-30 Bounded Synthesis for Safety Specs Homework 1
2 2020-04-07 Linear Temporal Logic Homework 2
3 2020-05-03 23:59 SMT Theory Homework 3
4 2020-05-10 23:59 Omega Automata Homework 4
5 2020-05-17 23:59 Bounded Synthesis Homework 5
6 2020-05-25  23:59 Games 1 Homework 6
7 2020-06-08  23:59 Games 2 Homework 7
8 2020-06-15  23:59 Relation Determinization Homework 8

Exercise Material

You find here the instructions for the exercise course.

Due Date Topic Instructions
2020-06-22 12:00 Bounded Synthesis for LTL Assignment 2


Administrative Information

All administrative information will be given in the first lecture. Please see the slides of lecture 1.


Roderick Bloem


View more