Přístupnostní navigace
E-přihláška
Vyhledávání Vyhledat Zavřít
Detail předmětu
FIT-SAVAk. rok: 2023/2024
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.
Jazyk výuky
Počet kreditů
Garant předmětu
Zajišťuje ústav
Vstupní znalosti
Pravidla hodnocení a ukončení předmětu
Projekt zaměřený na 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.
Učební cíle
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.
Doporučená literatura
eLearning
Zařazení předmětu ve studijních plánech
obor MBS , libovolný ročník, zimní semestr, povinně volitelnýobor MBI , libovolný ročník, zimní semestr, volitelnýobor MIS , libovolný ročník, zimní semestr, povinně volitelnýobor MIN , libovolný ročník, zimní semestr, povinně volitelnýobor MMM , libovolný ročník, zimní semestr, povinnýobor MGM , libovolný ročník, zimní semestr, volitelnýobor MPV , libovolný ročník, zimní semestr, volitelný
specializace NBIO , libovolný ročník, zimní semestr, volitelnýspecializace NISD , libovolný ročník, zimní semestr, volitelnýspecializace NISY , libovolný ročník, zimní semestr, volitelnýspecializace NISY do 2020/21 , libovolný ročník, zimní semestr, volitelnýspecializace NIDE , libovolný ročník, zimní semestr, volitelnýspecializace NCPS , libovolný ročník, zimní semestr, volitelnýspecializace NSEC , libovolný ročník, zimní semestr, volitelnýspecializace NMAT , libovolný ročník, zimní semestr, povinnýspecializace NGRI , libovolný ročník, zimní semestr, volitelnýspecializace NNET , libovolný ročník, zimní semestr, volitelnýspecializace NVIZ , libovolný ročník, zimní semestr, volitelnýspecializace NSEN , libovolný ročník, zimní semestr, volitelnýspecializace NMAL , libovolný ročník, zimní semestr, volitelnýspecializace NHPC , libovolný ročník, zimní semestr, volitelnýspecializace NVER , libovolný ročník, zimní semestr, povinnýspecializace NEMB , libovolný ročník, zimní semestr, volitelnýspecializace NEMB do 2021/22 , libovolný ročník, zimní semestr, volitelnýspecializace NADE , libovolný ročník, zimní semestr, volitelnýspecializace NSPE , libovolný ročník, zimní semestr, volitelný
obor MSK , 2. ročník, zimní semestr, povinně volitelný
Přednáška
Vyučující / Lektor
Osnova
Projekt
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.
Výsledky projektu se odevzdávají formou technické zprávy, která má tři hlavní části:
Každá část cca 3--5 stran v podobném formátu jako diplomová práce, každá za 10 bodů, hodnoceno dle míry zpracování a originality.
Elektronické učební texty