Detail předmětu

Statická analýza a verifikace

FIT-SAVAk. rok: 2023/2024

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. 

Jazyk výuky

čeština

Počet kreditů

5

Garant předmětu

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

Zajišťuje ústav

Ústav inteligentních systémů (UITS)

Vstupní znalosti

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

Pravidla hodnocení a ukončení předmětu

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

    • Projekt zaměřený na 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.

    Učební cíle

    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.

    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.

    Doporučená 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.
    Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, 2008.
    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.
    Bradley, A.R., Manna, Z.: The Calculus of Computation: Decision Procedures with Applications to Verification, Springer, 2007.
    Clarke, E.M., Henzinger, Th.A., Veith, H., Bloem, R. (Eds.): Handbook of Model Checking, Springer International Publishing, 2018.
    Edmund, M.C., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, 2000.
    Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual, Addison-Wesley Professional, 2003.
    Chess, B., West,J.: Secure Programming with Static Analysis. Addison-Wesley Professional, 2007.
    Khedker, U., Sanyal, A., Sathe, B.: Data Flow Analysis: Theory and Practice, CRC Press, 2009.
    Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View, Springer, 2008.
    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.
    Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis, Springer-Verlag, 2005.
    Rival, X., Yi, K. Introduction to Static Analysis: An Abstract Interpretation Perspective. MIT Press, 2020.
    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.

    Elearning

    eLearning: aktuální otevřený kurz

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

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

      obor MBS , 0 ročník, zimní semestr, povinně volitelný
      obor MIS , 0 ročník, zimní semestr, povinně volitelný
      obor MIN , 0 ročník, zimní semestr, povinně volitelný
      obor MSK , 2 ročník, zimní semestr, povinně volitelný
      obor MPV , 0 ročník, zimní semestr, volitelný
      obor MGM , 0 ročník, zimní semestr, volitelný
      obor MBI , 0 ročník, zimní semestr, volitelný
      obor MMM , 0 ročník, zimní semestr, povinný

    • Program MITAI magisterský navazující

      specializace NSPE , 0 ročník, zimní semestr, volitelný
      specializace NBIO , 0 ročník, zimní semestr, volitelný
      specializace NSEN , 0 ročník, zimní semestr, volitelný
      specializace NVIZ , 0 ročník, zimní semestr, volitelný
      specializace NGRI , 0 ročník, zimní semestr, volitelný
      specializace NADE , 0 ročník, zimní semestr, volitelný
      specializace NISD , 0 ročník, zimní semestr, volitelný
      specializace NMAT , 0 ročník, zimní semestr, povinný
      specializace NSEC , 0 ročník, zimní semestr, volitelný
      specializace NISY do 2020/21 , 0 ročník, zimní semestr, volitelný
      specializace NCPS , 0 ročník, zimní semestr, volitelný
      specializace NHPC , 0 ročník, zimní semestr, volitelný
      specializace NNET , 0 ročník, zimní semestr, volitelný
      specializace NMAL , 0 ročník, zimní semestr, volitelný
      specializace NVER , 0 ročník, zimní semestr, povinný
      specializace NIDE , 0 ročník, zimní semestr, volitelný
      specializace NEMB , 0 ročník, zimní semestr, volitelný
      specializace NISY , 0 ročník, zimní semestr, volitelný
      specializace NEMB do 2021/22 , 0 ročník, zimní semestr, volitelný

    Typ (způsob) výuky

     

    Přednáška

    39 hod., nepovinná

    Vyučující / Lektor

    Ing. Tomáš Dacík
    Ing. Ondřej Lengál, Ph.D.
    prof. Ing. Tomáš Vojnar, Ph.D.

    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

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

    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.

    Výsledky projektu se odevzdávají formou technické zprávy, která má tři hlavní části:

    1. Popis nástroje, přičemž důraz je na matematické/algoritmické/věcné principy, na kterých nástroj stojí. Použití nástroje z uživatelského pohledu je možno uvést, ale v míře spíše menší, ideálně jako odrazový můstek pro popis principů.
    2. Popis reprodukovaných experimentů: jaké experimenty byly reprodukovány, s jakými výsledky, k jakým pokusům o modifikace došlo, jak dopadly. (Pokud žádné stávající experimenty nejsou dostupné, je možno je nahradit větším důrazem na níže uvedený bod.)
    3. Popis vlastních originálních experimentů: ideálně nad školními projekty, volně dostupným software apod. (Uměle vytvořené příklady jsou možné, ale ne úplně ideální, pokud neukazují něco zcela zásadního. Pouhá modifikace parametrů či dílčích částí stávajících experimentů spadá do výše uvedeného bodu.)

    Každá část cca 3--5 stran v podobném formátu jako diplomová práce, každá za 10 bodů, hodnoceno dle míry zpracování a originality.

    Elektronické učební texty

    T. Vojnar. Static Analysis and Verification: Introduction. 2022/23.
    sav-lecture-01.pdf 0.13 MB

    Elearning

    eLearning: aktuální otevřený kurz