Poslední úprava: Mgr. Šárka Stejskalová, Ph.D. (23.09.2021)
The course introduces some of the frameworks that have been proposed to formalize reasoning about programs, focusing on propositional dynamic logic and temporal logics.
Literatura
Poslední úprava: Mgr. Šárka Stejskalová, Ph.D. (23.09.2021)
[1] D. Harel, D. Kozen, and J. Tiuryn, Dynamic Logic. MIT Press, 2000. [2] J. E. Hopcroft, R. Motwani, and J. D. Ullman, Introduction to Automata Theory, Languages, and Computation, 3rd Edition. Pearson Education, 2007. [3] M. Huth and M. Ryan, Logic in Computer Science. Modelling and Reasoning about Systems, 2nd edition. Cambridge University Press, 2004.
Sylabus
Poslední úprava: Mgr. Šárka Stejskalová, Ph.D. (23.09.2021)
1. Modal logic 2. Operational semantics of programs and program verification 3. Finite automata and regular expressions 4. Propositional dynamic logic 5. Kleene algebra and Kleene algebra with tests 6. Temporal logics and model checking 7. Automata-theoretic techniques in logics of programs