Lectures:
  Thu 10:40, S10 (Pavel Parízek)
Labs:
  Thu 12:20, S10 (Pavel Parízek)
Information in SIS: NSWI132
Term: Credit and exam

News

Slides

Lectures

Date Title Downloads
21.2.2019 Introductory lecture lecture00.pdf
28.2.2019 Model Checking Programs lecture01.pdf
7.3.2019 Concurrency Errors lecture02.pdf
14.3.2019 Symbolic Execution, Dynamic Analysis lecture03.pdf
21.3.2019 Deductive Methods, Bounded Model Checking lecture04.pdf
28.3.2019 Abstraction lecture05.pdf
4.4.2019 Contracts: Specification and Verification lecture06.pdf
25.4.2019 Static Analysis: Pointers and Heap Structures lecture08.pdf
2.5.2019 Abstract Interpretation lecture09.pdf
9.5.2019 Combining Verification Approaches lecture10.pdf
16.5.2019 Program Termination lecture11.pdf
23.5.2019 Program Synthesis lecture12.pdf

Labs

Date Title Downloads
28.2.2019 Java PathFinder lab01.pdf
7.3.2019 Detecting Concurrency Errors with JPF lab02.pdfconcur_bench.zip
14.3.2019 Symbolic PathFinder, RoadRunner lab03.pdf
21.3.2019 SMT Solvers, CBMC lab04.pdfsmt-examples.zipbmc-examples.zip
28.3.2019 CEGAR lab05.pdfcegar.tgz
4.4.2019 Code Contracts, Viper lab06.pdfcontracts-examples.zip
18.4.2019 T.J. Watson Libraries for Analysis lab07.pdfwala-examples.zip
25.4.2019 Static Analysis Tools lab08.pdfpredator-examples.tgz
2.5.2019 Realistic Verification Scenarios lab09.pdf

Annotation

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).

Syllabus

Organization

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
4.4.2019 23:59 Java Pathfinder hw1-jpf.pdfdaisyfs.zipelevator.ziprepworkers.zip
2.5.2019 23:59 Code Contracts hw2-contracts.pdf
24.5.2019 23:59 Static Analysis hw3-static.pdf
30.6.2019 23:59 Finding Bugs in Real Software hw4-realsw.pdf
23.5.2019 Research Papers hw5-papers.pdf

Grading

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

References

Archive


Academic year 2015/2016: lectures labs tools & examples