Detail předmětu

Formální analýza programů

FIT-FADAk. rok: 2022/2023

Přehled různých metod analýzy a verifikace programů s formálními základy. Model checking: základní principy, specifikace ověřovaných vlastností, temporální logiky, problém stavové exploze a jeho řešení, binární rozhodovací diagramy, automatizovaná abstrakce (a to zejména predikátová abstrakce klíčová v analýze programů). Různé přístupy ke statické analýze: analýza toku dat, ukazatelové analýzy, analýza s využitím omezení, typová analýza, abstraktní interpretace. Deduktivní verifikace, řešení SAT a SMT problémů, symbolická exekuce. Dynamická analýza s formálními základy, algoritmy jako FastTrack či dynamická redukce založená na částečném uspořádání.

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. CTL model checking.
4. Binární rozhodovací diagramy.
5. Predikátová abstrakce.
6. Abstraktní interpretace.
7. Analýza toku dat.
8. Řešení SAT a SMT problémů.
9. Symbolická exekuce.
10. Deduktivní verifikace.

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.

Základní 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 

Doporučená literatura

Aho, A.V., Lam, S., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison Wesley, 2nd ed., 2006. (Část věnovaná statické analýze.)
Ben-Ari, M.: Principles of the Spin Model Checker, Springer, 2008.
Bradley, A.R., Manna, Z.: The Calculus of Computation: Decision Procedures with Applications to Verification, Springer, 2007.
Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual, Addison-Wesley Professional, 2003.
Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View, Springer, 2008.
Materiály aktuálně volně dostupné na Internetu, a to zejména články a dokumentace týkající se počítačových nástrojů pro formální analýzu a verifikaci.
Moller, A., Schwartzbach, M.I.: Static Program Analysis, Department of Computer Science, Aarhus University, Denmark, 2018.
Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis, Springer-Verlag, 2005.
Soubor materiálů prezentovaných na přednáškách a zveřejněných přes WWW.

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

  • Program DIT doktorský 0 ročník, zimní semestr, povinně volitelný
  • Program DIT doktorský 0 ročník, zimní semestr, povinně volitelný
  • Program DIT-EN doktorský 0 ročník, zimní semestr, povinně volitelný
  • Program DIT-EN doktorský 0 ročník, zimní semestr, povinně volitelný

  • 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ý

  • 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.
Ing. Ondřej Lengál, 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: základní principy, specifikace ověřovaných vlastností, temporální logiky.
  3. LTL model checking s využitím automatů.
  4. Problém stavové exploze a jeho řešení, efektivní ukládání stavových prostorů, binární rozhodovací diagramy.
  5. Redukce stavových prostorů, zejména redukce na základě částečného uspořádání akcí.
  6. Automatizovaná abstrakce, a to zejména predikátová abstrakce, Craigovy interpolanty.
  7. Symbolická exekuce.
  8. Deduktivní verifikace.
  9. Řešení SAT a SMT problémů.
  10. Statická analýza založená na analýze toku dat, ukazatelové analýzy.
  11. Statická analýza založená na omezeních, typová analýza.
  12. Abstraktní interpretace.
  13. Dynamická analýza s formálními základy, algoritmy jako FastTrack, dynamická redukce na základě částečného uspořádání.

Konzultace v kombinovaném studiu

26 hod., nepovinná

Vyučující / Lektor

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