Předmět Formální analýza programů (FIT-FAD)

Na serveru studentino.cz naleznete nejrůznější studijní materiály: zápisky z přednášek nebo cvičení, vzorové testy, seminární práce, domácí úkoly a další z předmětu FIT-FAD - Formální analýza programů, Fakulta informačních technologií, Vysoké učení technické v Brně (VUT).

Materiál	Typ	Datum	Počet stažení

Cíl

Cílem předmětu je seznámit studenty s principy, možnostmi a omezeními aktuálně nejúspěšnějších metod známých, resp. zkoumaných, v oblasti aplikace formálních technik pro automatickou analýzu a verifikaci programů.

Osnova

Osnova přednášek:Přehled existujících metod analýzy a verifikace programů s formálními základy, jejich možnosti, výhody a nevýhody. Model checking konečně stavových systémů: základní princip, specifikace ověřovaných vlastností, temporální logiky. Problém stavové exploze a jeho řešení, efektivní ukládání stavových prostorů, redukce stavových prostorů. Modulární verifikace, automatizovaná abstrakce, a to zejména predikátová abstrakce, Craigovy interpolanty. Model checking nekonečně stavových systémů: řezy, symbolická verifikace, abstrakce, automatizovaná indukce. Dokazování teorémů. SAT solving, SMT solving. Statická analýza založená na analýze toku dat. Statická analýza založená na omezeních. Typová analýza. Metapřeklad. Abstraktní interpretace. Dynamická analýza s formálními základy, algoritmy jako Eraser či Daikon, využití metod automatizovaného učení v dynamické analýze. Osnova ostatní - projekty, práce:Prostudování vybraného vědeckého článku (nebo článků) z oblasti model checkingu, dokazování teorémů, statické či dynamické analýzy programů a jeho (jejich) zpracování do podoby tématické práce.

Literatura

Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking, MIT Press, 2000. ISBN 0-262-03270-8 Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis, Springer-Verlag, 2005. ISBN 3-540-65410-0 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.

Požadavky

Znalost základních pojmů z oblasti logiky, algebry, grafů, teorie formálních jazyků a automatů, překladačů a vyčíslitelnosti a složitosti.

Garant

prof. Ing. Tomáš Vojnar, Ph.D.

Vyučující

prof. Ing. Tomáš Vojnar, Ph.D.