Přístupnostní navigace
E-přihláška
Vyhledávání Vyhledat Zavřít
Detail předmětu
FIT-SAVAk. rok: 2019/2020
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
Výsledky učení předmětu
Prerekvizity
Způsob a kritéria hodnocení
Učební cíle
Doporučení literatura
Zařazení předmětu ve studijních plánech
specializace NVER , 0 ročník, zimní semestr, povinnýspecializace NMAT , 0 ročník, zimní semestr, povinnýspecializace NBIO , 0 ročník, zimní semestr, volitelný
obor MBI , 0 ročník, zimní semestr, volitelnýobor MBS , 0 ročník, zimní semestr, povinně volitelnýobor MGM , 0 ročník, zimní semestr, volitelnýobor MIN , 0 ročník, zimní semestr, povinně volitelnýobor MIS , 0 ročník, zimní semestr, povinně volitelnýobor MMI , 0 ročník, zimní semestr, volitelnýobor MSK , 2 ročník, zimní semestr, povinně volitelnýobor MMM , 0 ročník, zimní semestr, povinnýobor MPV , 0 ročník, zimní semestr, volitelný
specializace NSEN , 0 ročník, zimní semestr, volitelnýspecializace NVIZ , 0 ročník, zimní semestr, volitelnýspecializace NGRI , 0 ročník, zimní semestr, volitelnýspecializace NISD , 0 ročník, zimní semestr, volitelnýspecializace NSEC , 0 ročník, zimní semestr, volitelnýspecializace NCPS , 0 ročník, zimní semestr, volitelnýspecializace NHPC , 0 ročník, zimní semestr, volitelnýspecializace NNET , 0 ročník, zimní semestr, volitelnýspecializace NMAL , 0 ročník, zimní semestr, volitelnýspecializace NIDE , 0 ročník, zimní semestr, volitelnýspecializace NEMB , 0 ročník, zimní semestr, volitelnýspecializace NSPE , 0 ročník, zimní semestr, volitelnýspecializace NADE , 0 ročník, zimní semestr, volitelnýspecializace NISY , 0 ročník, zimní semestr, volitelný
Přednáška
Vyučující / Lektor
Osnova
Projekt
Elektronické učební texty