Statická analýza a verifikace

• 39 hod. přednášky
• 13 hod. projekty

• 60 bodů závěrečná zkouška
• 40 bodů projekty

Studenti jsou obeznámení s principy a metodami statické analýzy a verifikace a s jejím využitím při návrhu počítačových systémů. Studenti znají možnosti a základní způsoby použití počítačových nástrojů, které statickou analýzu a verifikaci podporují.
Získané povědomí o významu a možnostech uplatnění metod a nástrojů statické analýzy a verifikace při vývoji různých typů systémů a o jejich rostoucím nasazení v praxi.

Cílem předmětu je seznámit studenty s různými metodami statické analýzy a verifikace často používanými v praxi pro vyhledávání chyb, případně i pro automatizované dokazování korektnosti systémů. Studenti by se měli v předmětu seznámit s principy různých metod statické analýzy a verifikace, jejich výhodami a nevýhodami, ale také alespoň přehledově s existující nástrojovou podporou představených metod. V neposlední řadě by si studenti měli vyzkoušet v rámci projektů vybrané nástroje i prakticky.

Předmět seznámí studenty s metodami a nástroji statické analýzy a verifikace, které patří mezi stále častěji nasazované přístupy k zajištění patřičné kvality počítačových systémů. Znalost těchto metod je přínosem pro vývojáře software i hardware a obzvláště důležitá je pro působení v oblasti zajištění kvality (quality assurance).

Předpokládají se znalosti diskrétní matematiky, teorie formálních jazyků a algoritmizace na bakalářské úrovni.

• 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.
• Ben-Ari, M.: Principles of the Spin Model Checker, Springer, 2008.
• Soubor materiálů prezentovaných na přednáškách a zveřejněných přes WWW.
• Rival, X., Yi, K. Introduction to Static Analysis: An Abstract Interpretation Perspective. MIT Press, 2020.
• 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 statickou analýzu a verifikaci.
• Clarke, E.M., Henzinger, Th.A., Veith, H., Bloem, R. (Eds.): Handbook of Model Checking, Springer International Publishing, 2018.
• Moller, A., Schwartzbach, M.I.: Static Program Analysis, Department of Computer Science, Aarhus University, Denmark, 2018.

1. Význam pojmů analýza a verifikace. Klasifikace ověřovaných vlastností a ověřovaných systémů. Přehled přístupů ke statické analýze a verifikaci.
2. Temporální logiky CTL*, CTL a LTL.
3. Model checking systémů s vlastnostmi specifikovanými v LTL s využitím Büchiho automatů.
4. Model checking s využitím predikátové abstrakce postupně zjemňované na základě vylučování chybných protipříkladů.
5. Abstraktní interpretace I: základní pojmy a principy.
6. Abstraktní interpretace II: vybrané abstraktní domény úspěšné v praxi.
7. Základní pojmy a principy analýzy toku dat, klasické analýzy toku dat.
8. Pokročilejší analýzy toku dat, ukazatelové analýzy.
9. Verifikace software s využitím symbolického provádění.
10. Deduktivní verifikace anotovaných programů.
11. Řešení problémů SAT a SMT jako základ mnoha přístupů k analýze a verifikaci.
12. Binární rozhodovací diagramy.
13. Verifikace konečnosti běhu programů, automatizovaná analýza výpočetní složitosti.

Bližší seznámení se s vybraným nástrojem pro statickou analýzu a verifikaci a principy, na nichž je založen, reprodukce dostupných případových studií pro zvolený nástroj, vlastní experimenty s uvedeným nástrojem, sepsání technické zprávy o zvoleném nástroji a provedených experimentech.

• Jeden opravovaný projekt za 30 bodů. 
• Závěrečná zkouška za 70 bodů. 
• Podmínka zápočtu: min. 15 bodů získaných v průběhu semestru.

Získání alespoň 50% možného bodového zisku z projektu.