Syllabus
1. Modal logic2. Operational semantics of programs and program verification3. Finite automata and regular expressions4. Propositional dynamic logic5. Kleene algebra and Kleene algebra with tests6. Temporal logics and model checking7. Automata-theoretic techniques in logics of programs
Annotation
The course introduces some of the frameworks that have been proposed to formalize reasoning about programs, focusing on propositional dynamic logic and temporal logics.