Formální analýza a verifikace

• 39 hod. přednášky
• 13 hod. projekty

• 70 bodů závěrečná zkouška (testová část)
• 30 bodů projekty

Studenti jsou obeznámení s principy a metodami formální analýzy a verifikace a s jejím využitím při návrhu systémů, u nichž je kladen důraz na jejich korektní funkčnost. Studenti znají možnosti a základní způsoby použití počítačových nástrojů, které formální analýzu a verifikaci podporují.
Získané povědomí o významu a možnostech uplatnění formálních metod při vývoji různých typů systémů a o jejich rostoucím nasazení v praxi.

Cílem předmětu je představit studentům formální analýzu a verifikaci jako moderní a perspektivní metodu automatizovaného ověřování vlastností různých typů systémů, u nichž je kladen důraz na bezchybnou funkci (např. ovladačů a jiných částí operačních systémů, řídících programů, workflow, komunikačních protokolů, částí hardware apod.). Předmět seznamuje studenty jak s teoretickými základy dané oblasti, s počítačovými nástroji na nich založenými, tak i s úspěšnými aplikacemi formální analýzy a verifikace v praxi (Microsoft, Intel, Nasa, Airbus, ...).

Předpokládají se znalosti diskrétní matematiky, teorie formálních jazyků a algoritmizace na bakalářské úrovni.

volně dostupné

• Spin, SDV/Slam, CPAChecker, UFO, SatAbs, CBMC, LLBMC, Blast, Terminator, Java PathFinder, SMV, ABC, Uclid, Uppaal, Prism, FindBugs, Cppcheck, Predator, Forester, KLEE, Yogi, Coq, Vampire, Lingeling, Z3, MathSAT, VCC, ConTest, ANaConDA, ...

• Aho, A.V., Lam, S., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison Wesley, 2nd ed., 2006. The part devoted to static analysis.
• Bradley, A.R., Manna, Z.: The Calculus of Computation: Decision Procedures with Applications to Verification, Springer, 2007.
• Valmari, A.: The State Explosion Problem. In Reisig, W., Rozenberg, G.: Lectures on Petri Nets I: Basic Models, volume 1491 of Lecture Notes in Computer Science, pages 429-528. Springer-Verlag, 1998.
• Chess, B., West,J.: Secure Programming with Static Analysis. Addison-Wesley Professional, 2007.
• Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View, Springer, 2008.
• Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual, Addison-Wesley Professional, 2003.
• Ben-Ari, M.: Principles of the Spin Model Checker, Springer, 2008.
• Bertot Y., Castéran, P.: Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions, Springer, 2010.
• Materials presented within the lectures and made accessible via the Internet.
• Materials freely accessible on the Internet, especially papers and documentation related to the various computer-aided tools for formal analysis and verification.
• Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, 2008.
• Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis, Springer-Verlag, 2005.
• Edmund, M.C., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, 2000.
• Khedker, U., Sanyal, A., Sathe, B.: Data Flow Analysis: Theory and Practice, CRC Press, 2009.

1. Vymezení pojmu "formální analýza a verifikace". Možnosti a přínos formální analýzy a verifikace. Různé přístupy k formální analýze a verifikaci: model checking, statická analýza, dokazování teorémů.
2. Stavový prostor, cesty stavovým prostorem, abstrakce stavů a přechodů. Prokládání a paralelismus. Lineární a větvící se logický čas. Bezpečnost, živost a spravedlivost.
3. Temporální logiky CTL a CTL*, model checking systémů s vlastnostmi specifikovanými v těchto logikách s využitím explicitně reprezentovaných stavových prostorů.
4. Binární rozhodovací diagramy pro úspornou symbolickou reprezentaci stavových prostorů a jejich implementace.
5. Svazy, pevné body, Knaster-Tarského věta jako teoretický základ pro symbolický model checking.
6. Symbolický model checking pro CTL a CTL*.
7. Temporální logika LTL, korespondence mezi Büchi automaty a formulemi LTL, model checking systémů s vlastnostmi specifikovanými v LTL s využitím Büchiho automatů.
8. Redukce stavových prostorů na základě částečného uspořádaní akcí prováděných systémem. Přehled dalších přístupů k redukci stavových prostorů (symetrie, kompozitní verifikace apod.).
9. Metody automatizované abstrakce systémů, predikátová abstrakce, postupné zjemňování abstrakce na základě vylučování chybných protipříkladů, Craigova interpolace.
10. Rozhodovací procedury a moderní metody řešení problémů SAT a SMT a jejich využití ve formální verifikaci (např. v rámci predikátové abstrakce).
11. Klasické analýzy toku dat (živé proměnné, dostupné výrazy apod.) i některé vybrané pokročilé analýzy toku dat (např. některé analýzy ukazatelů), jejich popis pomocí tokových rovnic, metody iterativního řešení těchto rovnic.
12. Abstraktní interpretace a její využití pro definici statických analýz.
13. Statická analýza založená na vyhledávání chybových vzorů, zmínka o metodách dynamické analýzy (zejména pro potřeby detekce chyb v paralelismech).

• Projekt zahrnující nainstalování zvoleného nástroje pro automatickou verifikaci na formálním základě (Spin, Blast, ARMC, SMV, JPF, FindBugs, Invader, Uppaal aj.), experimenty s tímto nástrojem a sepsání eseje krátce popisující princip činnosti zvoleného nástroje (10b.) a provedené experimenty (10b. za experimenty na stávajících případových studiích, 10b. za nové případové studie). Po domluvě je možno se zaměřit i na nástroj založený na principech, které nejsou součástí přednášek (dokazování teorémů, systémy pracující v reálném časy apod.).

• Jeden opravovaný projekt za 30 bodů.
• Závěrečná zkouška za 70 bodů.
• Podmínka zápočtu: min. 15 bodů získaných v průběhu semestru.
• 
  Podmínky zápočtu:
  Získání alespoň 50% možného bodového zisku z projektu.

Získání alespoň 50% možného bodového zisku z projektu.