Detail předmětu
Formální analýza programů
FAD Ak. rok 2008/2009 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.
Garant předmětu
Jazyk výuky
Zakončení
Rozsah
- 26 hod. přednášky
Zajišťuje ústav
Přednášející
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í
Metody vyučování závisí na způsobu výuky a jsou popsány článkem 7 Studijního a zkušebního řádu VUT.
Kontrolovaná výuka
Přednášky a zpracování projektu.