Detail předmětu
Formální analýza programů
FAD Ak. rok 2013/2014 zimní semestr
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ů.
Garant předmětu
Jazyk výuky
Zakončení
Rozsah
- 26 hod. přednášky
Zajišťuje ústav
Získané dovednosti, znalosti a kompetence z předmětu
Znalost možností, omezení a principů současných metod analýzy programů s formálními základy. Schopnost jejich aplikace v pokročilých projektech a přehled o možnostech jejich dalšího rozvoje.
Prohloubení schopnosti číst a vytvářet formální zápisy.
Cíle předmětu
Cílem předmětu je seznámit studenty s principy, možnostmi a omezeními aktuálně nejúspěšnějších metod známých, resp. zkoumaných, v oblasti aplikace formálních technik pro automatickou analýzu a verifikaci programů.
Požadované prerekvizitní znalosti a dovednosti
Znalost základních pojmů z oblasti logiky, algebry, grafů, teorie formálních jazyků a automatů, překladačů a vyčíslitelnosti a složitosti.
Literatura studijní
- Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking, MIT Press, 2000. ISBN 0-262-03270-8
- Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis, Springer-Verlag, 2005. ISBN 3-540-65410-0
Osnova přednášek
- Přehled existujících metod analýzy a verifikace programů s formálními základy, jejich možnosti, výhody a nevýhody.
- Model checking konečně stavových systémů: základní princip, 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, Craigovy interpolanty.
- Model checking nekonečně stavových systémů: řezy, symbolická verifikace, abstrakce, automatizovaná indukce.
- Dokazování teorémů.
- SAT solving, SMT solving.
- Statická analýza založená na analýze toku dat.
- Statická 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.
Průběžná kontrola studia
Hodnocení studia je založeno na bodovacím systému. Pro úspěšné absolvování předmětu je nutno dosáhnout 50 bodů.
Metody vyučování
Výuka předmětu je realizována formou: Přednáška - 2 vyučovací hodiny týdně.
Kontrolovaná výuka
Přednášky a zpracování projektu.
Zařazení předmětu ve studijních plánech