Last update: 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.
Literature - Czech
Last update: 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.
Syllabus - Czech
Last update: 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