Detail předmětu

Formální analýza programů

FAD Ak. rok 2020/2021 zimní semestr

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.

Garant předmětu

Zástupce garanta předmětu

Jazyk výuky

český

Zakončení

zkouška (kombinovaná)

Rozsah

26 hod. přednášky

Bodové hodnocení

70 zkouška, 30 projekty

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.

Dovednosti, znalosti a kompetence obecné

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., Henzinger, Th.A., Veith, H., Bloem, R. (Eds.): Handbook of Model Checking, Springer International Publishing, 2018.
  • Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, 2008. 
  • Rival, X., Yi, K.: Introduction to Static Analysis. An Abstract Interpretation Perspective. MIT Press, 2020.
  • Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis, Springer-Verlag, 2005. 
  • Edmund, M.C., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, 2000. 
  • Moller, A., Schwartzbach, M.I.: Static Program Analysis, Department of Computer Science, Aarhus University, Denmark, 2018.
  • 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.) 
  • Bradley, A.R., Manna, Z.: The Calculus of Computation: Decision Procedures with Applications to Verification, Springer, 2007. 
  • Valmari, A.: The State Explosion Problem. In Reisig, W., Rozenberg, G.: Lectures on Petri Nets I: Basic Models, volume 1491 of Lecture Notes in Computer Science, pages 429-528. Springer-Verlag, 1998. 
  • Chess, B., West,J.: Secure Programming with Static Analysis. Addison-Wesley Professional, 2007. 
  • Khedker, U., Sanyal, A., Sathe, B.: Data Flow Analysis: Theory and Practice, CRC Press, 2009. 
  • Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View, Springer, 2008. 
  • Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual, Addison-Wesley Professional, 2003. 
  • Ben-Ari, M.: Principles of the Spin Model Checker, Springer, 2008. 
  • Bertot Y., Castéran, P.: Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions, Springer, 2010. 
  • Soubor materiálů prezentovaných na přednáškách a zveřejněných přes WWW. 
  • 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.

Literatura referenční

  • Clarke, E.M., Henzinger, Th.A., Veith, H., Bloem, R. (Eds.): Handbook of Model Checking, Springer International Publishing, 2018.
  • Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, 2008.
  • Rival, X., Yi, K.: Introduction to Static Analysis. An Abstract Interpretation Perspective. MIT Press, 2020.
  • 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. 
  • Edmund, M.C., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, 2000. 
  • Khedker, U., Sanyal, A., Sathe, B.: Data Flow Analysis: Theory and Practice, CRC Press, 2009.

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: 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í.

Osnova ostatní - projekty, práce

  1. Prostudování vybraného vědeckého článku (nebo článků) z oblasti model checkingu, statické analýzy, deduktivní verifikace či dynamické analýzy programů a jeho (jejich) zpracování do podoby tématické práce, resp. přednášky.

Průběžná kontrola studia

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

Kontrolovaná výuka

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

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

  • Program VTI-DR-4, obor DVI4, libovolný ročník, volitelný
Nahoru