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
Koordinátor předmětu
Jazyk výuky
Zakončení
Rozsah
- 26 hod. přednášky
Bodové hodnocení
- 70 bodů závěrečná zkouška
- 30 bodů projekty
Zajišťuje ústav
Přednášející
Cvičí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.
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í
- 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.
Osnova přednášek
- 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.
- Model checking: základní principy, specifikace ověřovaných vlastností, temporální logiky.
- LTL model checking s využitím automatů.
- Problém stavové exploze a jeho řešení, efektivní ukládání stavových prostorů, binární rozhodovací diagramy.
- Redukce stavových prostorů, zejména redukce na základě částečného uspořádání akcí.
- Automatizovaná abstrakce, a to zejména predikátová abstrakce, Craigovy interpolanty.
- Symbolická exekuce.
- Deduktivní verifikace.
- Řešení SAT a SMT problémů.
- Statická analýza založená na analýze toku dat, ukazatelové analýzy.
- Statická analýza založená na omezeních, typová analýza.
- Abstraktní interpretace.
- Dynamická analýza s formálními základy, algoritmy jako FastTrack, dynamická redukce na základě částečného uspořádání.
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ý
- Program VTI-DR-4, obor DVI4, libovolný ročník, volitelný
- Program VTI-DR-4 (anglicky), obor DVI4, libovolný ročník, volitelný
- Program VTI-DR-4 (anglicky), obor DVI4, libovolný ročník, volitelný