Detail předmětu

Statická analýza a verifikace

FIT-SAVAk. rok: 2020/2021

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. 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 static analysis and verification.
Rival, X., Yi, K. Introduction to Static Analysis: An Abstract Interpretation Perspective. MIT Press, 2020.
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.

    Projekt

    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