Formal verification of computer systems

My course is mostly based on the wonderful book Principles of Model Checking by C. Baier and J.-P. Katoen.

For further information on the course organization, grading, exercise sets, project, tool presentations, see ULB Université Virtuelle.

Lectures (handouts)

  • Course outline. [PDF]
  • Chapter 1: Formal verification. [Slides]
  • Chapter 2: Modeling systems. [Slides]
  • Chapter 3: Linear temporal logic. [Slides]
  • Chapter 4: Computation tree logic. [Slides]
  • Chapter 5: Symbolic model checking. [Slides]
  • Chapter 6: Model checking probabilistic systems. [Slides]