Detail předmětu
Statická analýza a verifikace
FIT-SAVAk. rok: 2021/2022
Zavedení základních pojmů, jako jsou analýza a verifikace, formální analýza a verifikace, spolehlivost a úplnost, logický a fyzický čas, bezpečnost a živost apod. Přehled různých přístupů k statické analýze a verifikaci i dalších alternativních přístupů k verifikaci. Úvod do temporálních logik jako do jednoho z klasických mechanismů pro specifikaci ověřovaných vlastností systémů. Model checking pro logiku LTL s využitím Büchiho automatů. Využití automaticky zjemňované predikátové abstrakce jako jeden z nejúspěšnějších přístupů k model checkingu software. Abstraktní interpretace jako jedna z nejúspěšnějších metod statické analýzy: základní principy a algoritmy a přehled významných abstraktních domén. Analýza toku dat: základní pojmy a principy, klasické analýzy používané v optimalizujících překladačích, návrh vlastních analýz, ukazatelové analýzy. Řešení problémů SAT a SMT, které stojí za mnoha (nejen) verifikačními přístupy. Verifikace založená na symbolickém provádění, omezený model checking a k-indukce. Deduktivní verifikace anotovaných programů (vstupní a výstupní podmínky funkcí, invarianty cyklů). Binární rozhodovací diagramy pro efektivní ukládání (nejen) stavových prostorů. Úvod do automatizované verifikace konečnosti běhu programů (absence možného zacyklení) a automatizované analýzy složitosti.
Garant předmětu
Zajišťuje ústav
Výsledky učení předmětu
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.
Prerekvizity
Předpokládají se znalosti diskrétní matematiky, teorie formálních jazyků a algoritmizace na bakalářské úrovni.
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.
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.
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.
Rival, X., Yi, K. Introduction to Static Analysis: An Abstract Interpretation Perspective. MIT Press, 2020.
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.
Způsob a kritéria hodnocení
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.
Jazyk výuky
čeština
Cíl
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.
Zařazení předmětu ve studijních plánech
- Program IT-MGR-2 magisterský navazující
obor MBS , libovolný ročník, zimní semestr, 5 kreditů, povinně volitelný
obor MBI , libovolný ročník, zimní semestr, 5 kreditů, volitelný
obor MIS , libovolný ročník, zimní semestr, 5 kreditů, povinně volitelný
obor MIN , libovolný ročník, zimní semestr, 5 kreditů, povinně volitelný
obor MMM , libovolný ročník, zimní semestr, 5 kreditů, povinný
obor MGM , libovolný ročník, zimní semestr, 5 kreditů, volitelný
obor MPV , libovolný ročník, zimní semestr, 5 kreditů, volitelný - Program MITAI magisterský navazující
specializace NBIO , libovolný ročník, zimní semestr, 5 kreditů, volitelný
specializace NISD , libovolný ročník, zimní semestr, 5 kreditů, volitelný
specializace NISY do 2020/21 , libovolný ročník, zimní semestr, 5 kreditů, volitelný
specializace NISY , libovolný ročník, zimní semestr, 5 kreditů, volitelný
specializace NIDE , libovolný ročník, zimní semestr, 5 kreditů, volitelný
specializace NCPS , libovolný ročník, zimní semestr, 5 kreditů, volitelný
specializace NSEC , libovolný ročník, zimní semestr, 5 kreditů, volitelný
specializace NMAT , libovolný ročník, zimní semestr, 5 kreditů, povinný
specializace NGRI , libovolný ročník, zimní semestr, 5 kreditů, volitelný
specializace NNET , libovolný ročník, zimní semestr, 5 kreditů, volitelný
specializace NVIZ , libovolný ročník, zimní semestr, 5 kreditů, volitelný
specializace NSEN , libovolný ročník, zimní semestr, 5 kreditů, volitelný
specializace NMAL , libovolný ročník, zimní semestr, 5 kreditů, volitelný
specializace NHPC , libovolný ročník, zimní semestr, 5 kreditů, volitelný
specializace NVER , libovolný ročník, zimní semestr, 5 kreditů, povinný
specializace NEMB , libovolný ročník, zimní semestr, 5 kreditů, volitelný
specializace NADE , libovolný ročník, zimní semestr, 5 kreditů, volitelný
specializace NSPE , libovolný ročník, zimní semestr, 5 kreditů, volitelný - Program IT-MGR-2 magisterský navazující
obor MSK , 2. ročník, zimní semestr, 5 kreditů, povinně volitelný
Typ (způsob) výuky
Přednáška
39 hod., nepovinná
Vyučující / Lektor
Osnova
- 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.
- Temporální logiky CTL*, CTL a LTL.
- Model checking systémů s vlastnostmi specifikovanými v LTL s využitím Büchiho automatů.
- Model checking s využitím predikátové abstrakce postupně zjemňované na základě vylučování chybných protipříkladů.
- Abstraktní interpretace I: základní pojmy a principy.
- Abstraktní interpretace II: vybrané abstraktní domény úspěšné v praxi.
- Základní pojmy a principy analýzy toku dat, klasické analýzy toku dat.
- Pokročilejší analýzy toku dat, ukazatelové analýzy.
- Verifikace software s využitím symbolického provádění.
- Deduktivní verifikace anotovaných programů.
- Řešení problémů SAT a SMT jako základ mnoha přístupů k analýze a verifikaci.
- Binární rozhodovací diagramy.
- Verifikace konečnosti běhu programů, automatizovaná analýza výpočetní složitosti.
Projekt
13 hod., povinná
Vyučující / Lektor
Osnova
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.