Detail předmětu

Formální analýza programů

FIT-FADAk. rok: 2020/2021

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.

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.

Doporučená nebo povinná literatura

Aho, A.V., Lam, S., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison Wesley, 2nd ed., 2006. The part devoted to static analysis.
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.
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.
Materials presented within the lectures and made accessible via the Internet.
Materials freely accessible on the Internet, especially papers and documentation related to the various computer-aided tools for formal analysis and verification.
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.

Způsob a kritéria hodnocení

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

Jazyk výuky

čeština, angličtina

Cíl

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.

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

  • Program VTI-DR-4 doktorský

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

  • Program VTI-DR-4 doktorský

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

Typ (způsob) výuky

 

Přednáška

26 hod., nepovinná

Vyučující / Lektor

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

eLearning