Semester: summer 2023/24
Lectures: Tue 12:20, S10 (Pavel Parízek)
Labs: Tue 14:00, S10 (Pavel Parízek)
Page in SIS: NSWI132
Grading: Credit and exam




Date Title Downloads
20.2.2024 Introductory lecture lecture00.pdf
27.2.2024 Model Checking Programs lecture01.pdf
5.3.2024 Concurrency Errors lecture02.pdf
12.3.2024 Symbolic Execution, Dynamic Analysis lecture03.pdf
19.3.2024 Deductive Methods, Bounded Model Checking lecture04.pdf
26.3.2024 Abstraction lecture05.pdf
2.4.2024 Contracts: Specification and Verification lecture06.pdf
23.4.2024 Static Analysis: Overview, Data-Flow lecture07.pdf
23.4.2024 Static Analysis: Pointers and Heap Structures lecture08.pdf
30.4.2024 Abstract Interpretation lecture09.pdf
7.5.2024 Combining Verification Approaches lecture10.pdf
7.5.2024 Program Termination lecture11.pdf
21.5.2024 Program Synthesis lecture12.pdf


Date Title Downloads
27.2.2024 Java PathFinder lab01.pdf
5.3.2024 Detecting Concurrency Errors with JPF
12.3.2024 Tools for Symbolic Execution and Dynamic Analysis lab03.pdf
19.3.2024 SMT Solvers, CBMC
26.3.2024 CEGAR lab05.pdfcegar.tgz
2.4.2024 Contracts: Dafny, Viper
23.4.2024 T.J. Watson Libraries for Analysis
23.4.2024 Static Analysis Tools lab08.pdfpointers-examples.zippredator-examples.tgz
30.4.2024 Realistic Verification Scenarios lab09.pdf


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, Dafny, 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
2.4.2024 23:59 Java Pathfinder
30.4.2024 23:59 Contracts hw2-contracts.pdf
26.5.2024 23:59 Static Analysis hw3-static.pdf
30.6.2024 23:59 Finding Bugs in Real Software hw4-realsw.pdf
21.5.2024 Research Papers hw5-papers.pdf


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