Detail předmětu
Statická analýza a verifikace
FIT-SAVAk. rok: 2020/2021
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.
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 static analysis and verification.
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.
Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, 2008.
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í
Podmínky zápočtu:
Získání alespoň 50% možného bodového zisku z projektu.
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 MMI , libovolný ročník, zimní semestr, 5 kreditů, 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 , 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.
eLearning
eLearning: aktuální otevřený kurz