Detail předmětu

Formální analýza programů

FAD Ak. rok 2011/2012 zimní semestr

Aktuální akademický rok

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

Vojnar Tomáš, prof. Ing., Ph.D. (UITS)

Jazyk výuky

česky, anglicky

Zakončení

zkouška

Rozsah

  • 26 hod. přednášky

Zajišťuje ústav

Ústav inteligentních systémů (UITS)

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

  1. 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.
  2. Model checking konečně stavových systémů: základní princip, specifikace ověřovaných vlastností, temporální logiky.
  3. Problém stavové exploze a jeho řešení, efektivní ukládání stavových prostorů, redukce stavových prostorů.
  4. Modulární verifikace, automatizovaná abstrakce, a to zejména predikátová abstrakce, Craigovy interpolanty.
  5. Model checking nekonečně stavových systémů: řezy, symbolická verifikace, abstrakce, automatizovaná indukce.
  6. Dokazování teorémů.
  7. SAT solving, SMT solving.
  8. Statická analýza založená na analýze toku dat.
  9. Statická analýza založená na omezeních.
  10. Typová analýza.
  11. Metapřeklad.
  12. Abstraktní interpretace.
  13. 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ů.

Kontrolovaná výuka

Přednášky a zpracování projektu.

Nahoru