Statická analýza a verifikace

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

• 70 bodů závěrečná zkouška (písemná část)
• 30 bodů projekty

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.

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

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

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

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.

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.

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

Získání alespoň 50 % možného bodového zisku z projektu.

Primární kontakt emailem, pomocí kterého je možno si domluvit individuální konzultaci.