Detail předmětu

Statická analýza a verifikace

FIT-SAVAk. rok: 2022/2023

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)

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.

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.

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.

Vymezení kontrolované výuky a způsob jejího provádění a formy nahrazování zameškané výuky

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.

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

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 , libovolný ročník, zimní semestr, povinně volitelný
    obor MBI , libovolný ročník, zimní semestr, volitelný
    obor MIS , libovolný ročník, zimní semestr, povinně volitelný
    obor MIN , libovolný ročník, zimní semestr, povinně volitelný
    obor MMM , libovolný ročník, zimní semestr, povinný
    obor MGM , libovolný ročník, zimní semestr, volitelný
    obor MPV , libovolný ročník, zimní semestr, volitelný

  • Program MITAI magisterský navazující

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

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

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

Typ (způsob) výuky

 

Přednáška

39 hod., nepovinná

Vyučující / Lektor

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. (en)

eLearning

eLearning: aktuální otevřený kurz