Program Analysis and Code Verification - NSWI132
Title: Analýza programů a verifikace kódu
Guaranteed by: Department of Distributed and Dependable Systems (32-KDSS)
Faculty: Faculty of Mathematics and Physics
Actual: from 2020
Semester: summer
E-Credits: 5
Hours per week, examination: summer s.:2/2, C+Ex [HT]
Capacity: unlimited
Min. number of students: unlimited
4EU+: no
Virtual mobility / capacity: no
State of the course: taught
Language: English
Teaching methods: full-time
Teaching methods: full-time
Additional information:
Note: enabled for web enrollment
Guarantor: doc. RNDr. Pavel Parízek, Ph.D.
Class: Informatika Mgr. - volitelný
Classification: Informatics > Software Engineering
Is incompatible with: NSWX132
Is interchangeable with: NSWX132
Opinion survey results   Examination dates   SS schedule   Noticeboard   
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).
Last update: Katedry Tajemník (22.04.2013)
Literature -

E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking, MIT Press, 2000

F. Nielson, H. R. Nielson, and Chris Hankin. Principles of Program Analysis, Springer, 2005

D. Kroening and O. Strichman. Decision Procedures: An Algorithmic Point of View, Springer, 2008

Last update: T_KSI (23.02.2009)
Syllabus -

Model checking of programs

Detecting concurrency errors

Symbolic execution

Dynamic analysis

Introduction to deductive methods

  • SAT solvers, SMT solvers

Bounded model checking

Predicate abstraction and CEGAR

Selected applications of deductive methods in software verification

  • Verification of program code against contracts

Static analysis and its usage in program verification

Abstract interpretation

Combination of verification techniques

Program termination

Program synthesis

Last update: Parízek Pavel, doc. RNDr., Ph.D. (07.05.2024)