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: Tajemník Katedry (22.04.2013)
Základní principy automatické analýzy a verifikace programů (model checking, statická analýza, dynamická
analýza, a deduktivní metody) a jejich praktická aplikace (například hledání chyb ve vícevláknových programech).
Literature -
Last update: T_KSI (23.02.2009)
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)
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
Syllabus -
Last update: doc. RNDr. Pavel Parízek, Ph.D. (07.05.2024)
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: doc. RNDr. Pavel Parízek, Ph.D. (07.05.2024)
Model checking programů
Hledání chyb ve vícevláknových programech
Symbolické vykonávání
Dynamická analýza
Úvod do deduktivních metod
SAT solvers, SMT solvers
Omezený model checking
Predikátová abstrakce a CEGAR
Vybrané aplikace deduktivních metod ve verifikaci software
verifikace programů proti kontraktům
Statická analýza kódu a její použití ve verifikaci programů