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).
Poslední úprava: Tajemník Katedry (22.04.2013)
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).
Literatura -
Poslední úprava: 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
Poslední úprava: 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
Sylabus -
Poslední úprava: Tajemník Katedry (29.04.2014)
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ů
Abstraktní interpretace
Kombinace technik verifikace
Terminace programů
Syntéza programů
Poslední úprava: Tajemník Katedry (29.04.2014)
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
