Přístupnostní navigace
E-přihláška
Vyhledávání Vyhledat Zavřít
Detail předmětu
FIT-FADAk. rok: 2022/2023
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
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
Vymezení kontrolované výuky a způsob jejího provádění a formy nahrazování zameškané výuky
Základní literatura
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking, MIT Press, 2000. ISBN 0-262-03270-8
Berard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P., McKenzie, P.: Systems and Software Verification: Model-Checking Techniques and Tools, Springer-Verlag, 2001. ISBN 3-540-41523-8
Monin, J.F., Hinchey, M.G.: Understanding Formal Methods, Springer-Verlag, 2003. ISBN 1-852-33247-6
Valmari, A.: The State Explosion Problem. In Reisig, W., Rozenberg, G.: Lectures on Petri Nets I: Basic Models, Lecture Notes in Computer Science, č.1491, s. 429-528. Springer-Verlag, 1998. ISBN 3-540-65306-6
Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis, Springer-Verlag, 2005. ISBN 3-540-65410-0
Schwartzbach, M.I.: Lecture Notes on Static Analysis, BRICS, Department of Computer Science, University of Aarhus, Denmark, 2006.
Doporučená literatura
Zařazení předmětu ve studijních plánech
obor DVI4 , libovolný ročník, zimní semestr, volitelný
Přednáška
Vyučující / Lektor
Osnova
Konzultace v kombinovaném studiu