Název:

Statická analýza a verifikace

Zkratka:SAV
Ak.rok:2019/2020
Semestr:zimní
Studijní plán:
ProgramObor/
specializace
RočníkPovinnost
IT-MGR-2MBI-povinný
IT-MGR-2MBS-povinně volitelný - skupina B
IT-MGR-2MGM-volitelný
IT-MGR-2MIN-povinně volitelný - skupina B
IT-MGR-2MIS-povinně volitelný - skupina F
IT-MGR-2MMI-volitelný
IT-MGR-2MMM-povinný
IT-MGR-2MPV-volitelný
IT-MGR-2MSK2.povinně volitelný - skupina M
MITAINADE-volitelný
MITAINBIO-volitelný
MITAINCPS-volitelný
MITAINEMB-volitelný
MITAINGRI-volitelný
MITAINHPC-volitelný
MITAINIDE-volitelný
MITAINISD-volitelný
MITAINISY-volitelný
MITAINMAL-volitelný
MITAINMAT-povinný
MITAINNET-volitelný
MITAINSEC-volitelný
MITAINSEN-volitelný
MITAINSPE-volitelný
MITAINVER-povinný
MITAINVIZ-volitelný
Vyučovací jazyk:čeština
Kredity:5 kreditů
Ukončení:zápočet+zkouška
Výuka:
hod./sempřednáškasem./cvič.lab. cvič.poč. cvič.jiná
Rozsah:3900013
 zkouškatestycvičenílaboratořeostatní
Body:6000040
Garant:Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
Zástupce garanta:Lengál Ondřej, Ing., Ph.D. (UITS)
Přednášející:Lengál Ondřej, Ing., Ph.D. (UITS)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
Fakulta:Fakulta informačních technologií VUT v Brně
Pracoviště:Ústav inteligentních systémů FIT VUT v Brně
Rozvrh:
DenVýukaTýdenMístnostOdDoPSKSkupiny
ÚtpřednáškavýukyD105 18:0020:501MIT 2MIT xx
 
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.
Anotace:
  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ů). Úvod do automatizované verifikace konečnosti běhu programů (absence možného zacyklení) a automatizované analýzy složitosti. Statická analýza založená na chybových vzorech.
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.
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.
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).
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. Řešení problémů SAT a SMT jako základ mnoha přístupů k analýze a verifikaci.
  10. Verifikace software s využitím symbolického provádění.
  11. Deduktivní verifikace anotovaných programů.
  12. Verifikace konečnosti běhu programů, automatizovaná analýza výpočetní složitosti.
  13. Statická analýza založená na vyhledávání chybových vzorů.
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.
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.
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.
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.
 

Vaše IPv4 adresa: 34.204.36.101