Model Checking

This course dealt with the fully automatic verification of hardware and software using model checking algorithms and tools.

The topics included:

• Model checking algorithms for verifying temporal (safety, liveness and fairness) and regular properties
• Knowledge and applications of temporal logics (e.g., LTL, CTL and CTL*)
• Use of model checking tools (e.g., SMV, Spin and ProB)
• Basics of advanced methods (e.g., Binary Decision Diagrams (BDD), Partial Order Reduction (POR) or symmetry breaking)

I was the main teacher giving lectures and tutorials and grading students exams. I was involved in teaching this course for 2 years from 2018 until 2019.