Název:

Formální analýza programů

Zkratka:FAD
Ak.rok:2012/2013
Semestr:zimní
Studijní plán:
ProgramOborRočníkPovinnost
VTI-DR-4DVI4-volitelný
Vyučovací jazyk:čeština
Aktuální informace:POZOR! Změna místa konání 1. opravného termínu: bude se konat v A112.
Ukončení:zkouška (kombinovaná)
Výuka:
hod./sempřednáškasem./cvičenílab. cvičenípoč. cvičeníjiná
Rozsah:260000
 zkouškatestycvičenílaboratořeostatní
Body:1000000
Garant:Vojnar Tomáš, prof. Ing., Ph.D., UITS
Přednášející:Vojnar Tomáš, prof. Ing., Ph.D., UITS
Fakulta:Fakulta informačních technologií VUT v Brně
Pracoviště:Ústav inteligentních systémů FIT VUT v Brně
 
Cíle předmětu:
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ů.
Anotace:
Přehled různých metod analýzy a verifikace programů s formálními základy. Model checking konečně stavových systémů: základní principy, 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 klíčová v analýze programů). Model checking nekonečně stavových systémů: řezy, symbolická verifikace, abstrakce, automatizovaná indukce. Dokazování teorémů, SAT solving, SMT solving. Různé možnosti statické analýzy, analýza toku dat, 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.
Požadované prerekvizitní znalosti a dovednosti:
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.
Získané dovednosti, znalosti a kompetence z předmětu:
Znalost možností, omezení a principů současných metod analýzy programů s formálními základy. Schopnost jejich aplikace v pokročilých projektech a přehled o možnostech jejich dalšího rozvoje.
Dovednosti, znalosti a kompetence obecné:
Prohloubení schopnosti číst a vytvářet formální zápisy.
Osnova přednášek:
  1. 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.
  2. Model checking konečně stavových systémů: základní princip, specifikace ověřovaných vlastností, temporální logiky.
  3. Problém stavové exploze a jeho řešení, efektivní ukládání stavových prostorů, redukce stavových prostorů.
  4. Modulární verifikace, automatizovaná abstrakce, a to zejména predikátová abstrakce, Craigovy interpolanty.
  5. Model checking nekonečně stavových systémů: řezy, symbolická verifikace, abstrakce, automatizovaná indukce.
  6. Dokazování teorémů.
  7. SAT solving, SMT solving.
  8. Statická analýza založená na analýze toku dat.
  9. Statická analýza založená na omezeních.
  10. Typová analýza.
  11. Metapřeklad.
  12. Abstraktní interpretace.
  13. 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:
  1. 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 referenční:
  1. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking, MIT Press, 2000. ISBN 0-262-03270-8
  2. 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
  3. Monin, J.F., Hinchey, M.G.: Understanding Formal Methods, Springer-Verlag, 2003. ISBN 1-852-33247-6
  4. 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
  5. Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis, Springer-Verlag, 2005. ISBN 3-540-65410-0
  6. Schwartzbach, M.I.: Lecture Notes on Static Analysis, BRICS, Department of Computer Science, University of Aarhus, Denmark, 2006.
Literatura studijní:
  1. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking, MIT Press, 2000. ISBN 0-262-03270-8
  2. Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis, Springer-Verlag, 2005. ISBN 3-540-65410-0
Kontrolovaná výuka:
Přednášky a zpracování projektu.
Průběžná kontrola studia:
Diskuse v rámci přednášek, kontrola zpracování tématické práce.