Přehled různých metod analýzy a verifikace programů s formálními základy. Model checking konečně stavových systémů: základní principy, specifikace ověřovaných vlastností, temporální logiky, problém stavové exploze a jeho řešení, efektivní ukládání stavových prostorů, redukce stavových prostorů, modulární verifikace, automatizovaná abstrakce (a to zejména predikátová abstrakce klíčová v analýze programů). Model checking nekonečně stavových systémů: řezy, symbolická verifikace, abstrakce, automatizovaná indukce. Dokazování teorémů, SAT solving, SMT solving. Různé možnosti statické analýzy, analýza toku dat, analýza založená na omezeních, typová analýza, metapřeklad, abstraktní interpretace. Dynamická analýza s formálními základy, algoritmy jako Eraser či Daikon, využití metod automatizovaného učení v dynamické analýze.

Okruhy otázek k SDZ

1. Temporální logiky LTL, CTL a CTL*.
2. Büchiho automaty a model checking LTL s jejich využitím.
3. Explicitní model checking CTL.
4. Binární rozhodovací diagramy a symbolický model checking CTL na nich založený.
5. Redukce na základě částečného uspořádání.
6. Predikátová abstrakce.
7. Abstraktní interpretace.
8. Analýza toku dat.
9. Analýza aliasování ukazatelů.
10. Řešení SAT a SMT problémů.