Detail předmětu

Formální analýza programů

FIT-FADAk. rok: 2019/2020

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ů.

Jazyk výuky

čeština

Garant předmětu

prof. Ing. Tomáš Vojnar, Ph.D.

Zajišťuje ústav

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

Výsledky učení 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.

Prerekvizity

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.

Způsob a kritéria hodnocení

Diskuse v rámci přednášek, kontrola zpracování tématické práce.

Učební cíle

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ů.

Vymezení kontrolované výuky a způsob jejího provádění a formy nahrazování zameškané výuky

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

Doporučená literatura

Berard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P., McKenzie, P.: Systems and Software Verification: Model-Checking Techniques and Tools, Springer-Verlag, 2001. ISBN 3-540-41523-8
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking, MIT Press, 2000. ISBN 0-262-03270-8
Monin, J.F., Hinchey, M.G.: Understanding Formal Methods, Springer-Verlag, 2003. ISBN 1-852-33247-6
Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis, Springer-Verlag, 2005. ISBN 3-540-65410-0
Schwartzbach, M.I.: Lecture Notes on Static Analysis, BRICS, Department of Computer Science, University of Aarhus, Denmark, 2006.
Valmari, A.: The State Explosion Problem. In Reisig, W., Rozenberg, G.: Lectures on Petri Nets I: Basic Models, Lecture Notes in Computer Science, č.1491, s. 429-528. Springer-Verlag, 1998. ISBN 3-540-65306-6

Zařazení předmětu ve studijních plánech

  • Program VTI-DR-4 doktorský

    obor DVI4 , 0 ročník, zimní semestr, volitelný

  • Program VTI-DR-4 doktorský

    obor DVI4 , 0 ročník, zimní semestr, volitelný

Typ (způsob) výuky

 

Přednáška

26 hod., nepovinná

Vyučující / Lektor

prof. Ing. Tomáš Vojnar, Ph.D.

Osnova

  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.

Konzultace v kombinovaném studiu

26 hod., nepovinná

Vyučující / Lektor

prof. Ing. Tomáš Vojnar, Ph.D.