• 13. 2. 2023: Introduction
• 20. 2. 2023: Reachability in pushdown systems
• 27. 2. 2023: Partial order reduction (part I)
• 6. 3. 2023: Partial order reduction (part II)
• 13. 3. 2023: Abstraction (part I) [prerecorded, spring holidays]
  
• 20. 3. 2023: Abstraction (part II)
  
• 27. 3. 2023: Static analysis and abstract interpretation
• 3. 4. 2023: Shape analysis via 3-valued logic
• 17. 4. 2023: Verification via automata, symbolic execution, and interpolation
• 24. 4. 2023: Theorem prover ACL2 [no subject of final examination][self-study, no lecture]
• 15. 5. 2023: Property directed reachability (PDR/IC3)

Topics not covered by the course

• LTL model checking of pushdown systems
• Translation of LTL to Büchi automata
• Symbolic execution, backward symbolic execution, k-induction, fuzzing