Přístupnostní navigace
E-přihláška
Vyhledávání Vyhledat Zavřít
Detail předmětu
FIT-FADAk. rok: 2023/2024
Přehled různých metod analýzy a verifikace programů s formálními základy. Model checking: základní principy, specifikace ověřovaných vlastností, temporální logiky, problém stavové exploze a jeho řešení, binární rozhodovací diagramy, automatizovaná abstrakce (a to zejména predikátová abstrakce klíčová v analýze programů). Různé přístupy ke statické analýze: analýza toku dat, ukazatelové analýzy, analýza s využitím omezení, typová analýza, abstraktní interpretace. Deduktivní verifikace, řešení SAT a SMT problémů, symbolická exekuce. Dynamická analýza s formálními základy, algoritmy jako FastTrack či dynamická redukce založená na částečném uspořádání.Okruhy otázek k SDZ:1. Temporální logiky LTL, CTL a CTL*. 2. Büchiho automaty a model checking LTL s jejich využitím. 3. CTL model checking. 4. Binární rozhodovací diagramy. 5. Predikátová abstrakce. 6. Abstraktní interpretace. 7. Analýza toku dat. 8. Řešení SAT a SMT problémů. 9. Symbolická exekuce.10. Deduktivní verifikace.
Jazyk výuky
Garant předmětu
Zajišťuje ústav
Vstupní znalosti
Pravidla hodnocení a ukončení předmětu
Učební cíle
Základní literatura
Doporučení literatura
Zařazení předmětu ve studijních plánech
obor DVI4 , 0 ročník, zimní semestr, volitelný
Přednáška
Vyučující / Lektor
Osnova
Konzultace v kombinovaném studiu