čeština

Znalost možností, omezení a principů současných metod analýzy programů s formálními základy. Schopnost jejich aplikace v pokročilých projektech a přehled o možnostech jejich dalšího rozvoje.
Prohloubení schopnosti číst a vytvářet formální zápisy.

Znalost základních pojmů z oblasti logiky, algebry, grafů, teorie formálních jazyků a automatů, překladačů a vyčíslitelnosti a složitosti.

Diskuse v rámci přednášek, kontrola zpracování tématické práce.

Cílem předmětu je seznámit studenty s principy, možnostmi a omezeními aktuálně nejúspěšnějších metod známých, resp. zkoumaných, v oblasti aplikace formálních technik pro automatickou analýzu a verifikaci programů.

Přednášky a zpracování projektu.

Berard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P., McKenzie, P.: Systems and Software Verification: Model-Checking Techniques and Tools, Springer-Verlag, 2001. ISBN 3-540-41523-8 
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking, MIT Press, 2000. ISBN 0-262-03270-8 
Monin, J.F., Hinchey, M.G.: Understanding Formal Methods, Springer-Verlag, 2003. ISBN 1-852-33247-6 
Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis, Springer-Verlag, 2005. ISBN 3-540-65410-0 
Schwartzbach, M.I.: Lecture Notes on Static Analysis, BRICS, Department of Computer Science, University of Aarhus, Denmark, 2006. 
Valmari, A.: The State Explosion Problem. In Reisig, W., Rozenberg, G.: Lectures on Petri Nets I: Basic Models, Lecture Notes in Computer Science, č.1491, s. 429-528. Springer-Verlag, 1998. ISBN 3-540-65306-6 

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.)
Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, 2008.
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.
Bradley, A.R., Manna, Z.: The Calculus of Computation: Decision Procedures with Applications to Verification, Springer, 2007.
Clarke, E.M., Henzinger, Th.A., Veith, H., Bloem, R. (Eds.): Handbook of Model Checking, Springer International Publishing, 2018.
Edmund, M.C., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, 2000.
Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual, Addison-Wesley Professional, 2003.
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.
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 formální analýzu a verifikaci.
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.
Rival, X., Yi, K.: Introduction to Static Analysis. An Abstract Interpretation Perspective. MIT Press, 2020.
Soubor materiálů prezentovaných na přednáškách a zveřejněných přes WWW.
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.