DD2552 HT21 Seminars on Theoretical Computer Science, Programming Languages and Formal Methods (semteo21)

Short summary of the course

This seminar course covers the basics of formal specification and verification of probabilistic systems. It focuses in particular on verification using probabilistic logics such as PCTL of Markov processes, using model checking tools that use numeric-symbolic and statistical methods.

Examination and grades

The default examination in the course is through solving the set of homework problems in hw.pdf. The handed-in solutions are given a grade of A, B, C, D, E, FX, or F, which is also the student's grade on the course as a whole. Homework solutions must be sent as a PDF file to palmskog@kth.se by January 14, 2022, 23:59 CET, for the results to be reported to LADOK before the beginning of period 3 of the 2021/2022 academic year.

As a special one-time concession due to earlier issues in the course, students can elect to, instead of homework, take a 1-hour oral examination with the course lecturer during the winter exam week, January 10 to January 14. The oral exam will be given a grade of A, B, C, D, E, FX, or F, which is then the grade on the course as a whole. Students must contact palmskog@kth.se by December 22, 23:59 CET to book a time if they want to use this examination option. The oral examination will be about problems similar to the homework problems. 

Re-examination

The re-examination in the course during spring 2022 is by solving a new set of homework problems. The handed-in solutions are given a grade of A, B, C, D, E, FX, or F, which is also the grade on the course as a whole.

The re-examination homework problem set will appear on the course website on March 14, 2022.

The re-examination homework problem solutions must be sent to palmskog@kth.se by April 22, 2022, 23:59 CET, for the results to be reported into LADOK for the 2021/2022 academic year.

Intended learning outcomes and the examination

The intended learning outcomes are that after passing the course, the student shall be able to:

1. discuss advanced concepts within the area of the course
2. attack problems within the area of the course actively, both through own work and through search of relevant information
3. assimilate and present the essential contents of scientific articles within the area of the course.

In the homework problems, the intention is that different numbers of total points correspond to different degrees of outcome 2. Outcome 1 and 3 are also examined by the homework by the choice of problems and by the references to research literature.

Course literature

The main course literature is a survey on statistical model checking

Please contact palmskog@kth.se if you are unable to download a PDF copy of the survey.

Seminars