Selected Topics Design and Verification
Table of Content
Content
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 | Part1, Part2 |
| 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 | slides_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 | ||
Material
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.Lecturers
Bloem
Professor