Sylabus
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ů
Anotace
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).