čeština

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

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.

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.
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.
Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis, Springer-Verlag, 2005.
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.
Edmund, M.C., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, 2000.
Bradley, A.R., Manna, Z.: The Calculus of Computation: Decision Procedures with Applications to Verification, Springer, 2007.
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.