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: Katedry Tajemník (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).
Poslední úprava: Katedry Tajemník (22.04.2013)
Literatura -
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
Poslední úprava: T_KSI (23.02.2009)
Sylabus -
Model checking programů
Hledání chyb ve vícevláknových programech
Symbolické vykonávání
Dynamická analýza
Fuzz testování
Ú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
pokročilé aspekty 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: Parízek Pavel, doc. RNDr., Ph.D. (14.05.2024)
Model checking of programs
Detecting concurrency errors
Symbolic execution
Dynamic analysis
Fuzz testing
Introduction to deductive methods
SAT solvers, SMT solvers
Bounded model checking
Predicate abstraction and CEGAR
Selected applications of deductive methods in software verification
Advanced topics in verification of program code against contracts
Static analysis and its usage in program verification
Abstract interpretation
Combination of verification techniques
Program termination
Program synthesis
Poslední úprava: Parízek Pavel, doc. RNDr., Ph.D. (14.05.2024)