Detail předmětu

Statická analýza a verifikace

FIT-SAVAk. rok: 2019/2020

Zavedení základních pojmů, jako jsou analýza a verifikace, formální analýza a verifikace, spolehlivost a úplnost, logický a fyzický čas, bezpečnost a živost apod. Přehled různých přístupů k statické analýze a verifikaci i dalších alternativních přístupů k verifikaci. Úvod do temporálních logik jako do jednoho z klasických mechanismů pro specifikaci ověřovaných vlastností systémů. Model checking pro logiku LTL s využitím Büchiho automatů. Využití automaticky zjemňované predikátové abstrakce jako jeden z nejúspěšnějších přístupů k model checkingu software. Abstraktní interpretace jako jedna z nejúspěšnějších metod statické analýzy: základní principy a algoritmy a přehled významných abstraktních domén. Analýza toku dat: základní pojmy a principy, klasické analýzy používané v optimalizujících překladačích, návrh vlastních analýz, ukazatelové analýzy. Řešení problémů SAT a SMT, které stojí za mnoha (nejen) verifikačními přístupy. Verifikace založená na symbolickém provádění, omezený model checking a k-indukce. Deduktivní verifikace anotovaných programů (vstupní a výstupní podmínky funkcí, invarianty cyklů). Binární rozhodovací diagramy pro efektivní ukládání (nejen) stavových prostorů. Úvod do automatizované verifikace konečnosti běhu programů (absence možného zacyklení) a automatizované analýzy složitosti. 

Výsledky učení předmětu

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

Prerekvizity

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

Doporučená nebo povinná literatura

Aho, A.V., Lam, S., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison Wesley, 2nd ed., 2006. (Část věnovaná statické analýze.)
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.
Soubor materiálů prezentovaných na přednáškách a zveřejněných přes WWW.
Materiály aktuálně volně dostupné na Internetu, a to zejména články a dokumentace týkající se počítačových nástrojů pro statickou analýzu a verifikaci.
Clarke, E.M., Henzinger, Th.A., Veith, H., Bloem, R. (Eds.): Handbook of Model Checking, Springer International Publishing, 2018.
Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, 2008.
Moller, A., Schwartzbach, M.I.: Static Program Analysis, Department of Computer Science, Aarhus University, Denmark, 2018.
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.

Způsob a kritéria hodnocení

  • 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.

    Jazyk výuky

    čeština

    Cíl

    Cílem předmětu je seznámit studenty s různými metodami statické analýzy a verifikace často používanými v praxi pro vyhledávání chyb, případně i pro automatizované dokazování korektnosti systémů. Studenti by se měli v předmětu seznámit s principy různých metod statické analýzy a verifikace, jejich výhodami a nevýhodami, ale také alespoň přehledově s existující nástrojovou podporou představených metod. V neposlední řadě by si studenti měli vyzkoušet v rámci projektů vybrané nástroje i prakticky.

    Zařazení předmětu ve studijních plánech

    • Program IT-MGR-2 magisterský navazující

      obor MBS , libovolný ročník, zimní semestr, 5 kreditů, povinně volitelný
      obor MBI , libovolný ročník, zimní semestr, 5 kreditů, volitelný
      obor MIS , libovolný ročník, zimní semestr, 5 kreditů, povinně volitelný
      obor MIN , libovolný ročník, zimní semestr, 5 kreditů, povinně volitelný
      obor MMI , libovolný ročník, zimní semestr, 5 kreditů, volitelný
      obor MMM , libovolný ročník, zimní semestr, 5 kreditů, povinný
      obor MGM , libovolný ročník, zimní semestr, 5 kreditů, volitelný
      obor MPV , libovolný ročník, zimní semestr, 5 kreditů, volitelný

    • Program MITAI magisterský navazující

      specializace NBIO , libovolný ročník, zimní semestr, 5 kreditů, volitelný
      specializace NISD , libovolný ročník, zimní semestr, 5 kreditů, volitelný
      specializace NISY , libovolný ročník, zimní semestr, 5 kreditů, volitelný
      specializace NIDE , libovolný ročník, zimní semestr, 5 kreditů, volitelný
      specializace NCPS , libovolný ročník, zimní semestr, 5 kreditů, volitelný
      specializace NSEC , libovolný ročník, zimní semestr, 5 kreditů, volitelný
      specializace NMAT , libovolný ročník, zimní semestr, 5 kreditů, povinný
      specializace NGRI , libovolný ročník, zimní semestr, 5 kreditů, volitelný
      specializace NNET , libovolný ročník, zimní semestr, 5 kreditů, volitelný
      specializace NVIZ , libovolný ročník, zimní semestr, 5 kreditů, volitelný
      specializace NSEN , libovolný ročník, zimní semestr, 5 kreditů, volitelný
      specializace NMAL , libovolný ročník, zimní semestr, 5 kreditů, volitelný
      specializace NHPC , libovolný ročník, zimní semestr, 5 kreditů, volitelný
      specializace NVER , libovolný ročník, zimní semestr, 5 kreditů, povinný
      specializace NEMB , libovolný ročník, zimní semestr, 5 kreditů, volitelný
      specializace NADE , libovolný ročník, zimní semestr, 5 kreditů, volitelný
      specializace NSPE , libovolný ročník, zimní semestr, 5 kreditů, volitelný

    • Program IT-MGR-2 magisterský navazující

      obor MSK , 2. ročník, zimní semestr, 5 kreditů, povinně volitelný

    Typ (způsob) výuky

     

    Přednáška

    39 hod., nepovinná

    Vyučující / Lektor

    Osnova

    1. Význam pojmů analýza a verifikace. Klasifikace ověřovaných vlastností a ověřovaných systémů. Přehled přístupů ke statické analýze a verifikaci.
    2. Temporální logiky CTL*, CTL a LTL.
    3. Model checking systémů s vlastnostmi specifikovanými v LTL s využitím Büchiho automatů.
    4. Model checking s využitím predikátové abstrakce postupně zjemňované na základě vylučování chybných protipříkladů.
    5. Abstraktní interpretace I: základní pojmy a principy.
    6. Abstraktní interpretace II: vybrané abstraktní domény úspěšné v praxi.
    7. Základní pojmy a principy analýzy toku dat, klasické analýzy toku dat.
    8. Pokročilejší analýzy toku dat, ukazatelové analýzy.
    9. Verifikace software s využitím symbolického provádění.
    10. Deduktivní verifikace anotovaných programů.
    11. Řešení problémů SAT a SMT jako základ mnoha přístupů k analýze a verifikaci.
    12. Binární rozhodovací diagramy.
    13. Verifikace konečnosti běhu programů, automatizovaná analýza výpočetní složitosti.

    Projekty

    13 hod., povinná

    Vyučující / Lektor

    Osnova

    Bližší seznámení se s vybraným nástrojem pro statickou analýzu a verifikaci a principy, na nichž je založen, reprodukce dostupných případových studií pro zvolený nástroj, vlastní experimenty s uvedeným nástrojem, sepsání technické zprávy o zvoleném nástroji a provedených experimentech.

    eLearning