Detail předmětu

Statická analýza a verifikace

SAV Ak. rok 2019/2020 zimní semestr 5 kreditů

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. 

Garant předmětu

Zástupce garanta předmětu

Jazyk výuky

český

Zakončení

zápočet+zkouška

Rozsah

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

Bodové hodnocení

60 zkouška, 40 projekty

Zajišťuje ústav

Přednášející

Stránky předmětu

Získané dovednosti, znalosti a kompetence z 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í.

Dovednosti, znalosti a kompetence obecné

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.

Cíle předmětu

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.

Proč je předmět vyučován

Předmět seznámí studenty s metodami a nástroji statické analýzy a verifikace, které patří mezi stále častěji nasazované přístupy k zajištění patřičné kvality počítačových systémů. Znalost těchto metod je přínosem pro vývojáře software i hardware a obzvláště důležitá je pro působení v oblasti zajištění kvality (quality assurance).

Požadované prerekvizitní znalosti a dovednosti

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

Literatura studijní

  • 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. 
  • Moller, A., Schwartzbach, M.I.: Static Program Analysis, Department of Computer Science, Aarhus University, Denmark, 2018.
  • 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. 
  • 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. 
  • 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.

Literatura referenční

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

Osnova přednášek

  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.

Osnova ostatní - projekty, práce

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.

Průběžná kontrola studia

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

Rozvrh

DenTypTýdnyMístn.OdDoPSKSkupInfo
Pozkouška2020-01-06 E105 15:0017:50 1MIT 2MIT řádná
Pozkouška2020-01-20 E104 16:0018:50 1MIT 2MIT 1. oprava
Útzkouška2020-01-28 E104 12:0014:50 1MIT 2MIT 2. oprava
Útpřednáškavýuky E104 18:0020:50 1MIT 2MIT xx

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

Nahoru