Semester: summer 2020/21
Lectures: Mon 10:40, online (Pavel Parízek)
Labs: Mon 12:20, online (Pavel Parízek)
Page in SIS: NSWI132
Grading: Credit and exam




Date Title Downloads
1.3.2021 Introductory lecture lecture00.pdf


Date Title Downloads


Basic principles of automated analysis and verification of programs (model checking, static analysis, dynamic analysis, and deductive methods) and their practical applications (e.g., detecting concurrency errors).



During the lectures we will describe individual program verification and analysis methods, including basic concepts, main algorithms, and their limitations.

The purpose of the lab is to provide students with a hand-on experience with selected verification and analysis tools ( Java Pathfinder, CBMC, Code Contracts, WALA, ...).

Homework assignments

There will be five assignments, each taking approximately 10-15 hours of homework. You need to do the assignment no. 5 (presentation of some research publication) and two others to get credit (“zápočet”).
Note: 10% of your score will be deducted for every calendar day your solution of the assignment is late. This implies that no solutions will be accepted after 10 calendar days past its due date.

Date Title Downloads


Final grades will depend on the quality of your homework and on the result of the voluntary final exam as follows:

Grades will be based on points in the following way:

Grade Required points
Excellent:85-125 points
Very good:72-84 points
Good: 60-71 points



Academic year 2015/2016: lectures labs tools & examples