Model Checking


  • 2005-12-23: no lecture (I am sick)
  • 2005-11-25: no excercise course (to synchronize with course)
  • 2005-11-23: double lecture feature

  • 2005-11-16: no lecture course (no change for execerise course on friday)

  • 2005-10-24: new schedule and location

Hours per week: 2 course + 1 excercise course

ECTS Credits: 4

Dr. Martin Leucker, Course
Jewgenij Botaschanjan, Excercise course

Study programs:
Informatik (Master) ab 1–3
Informatik (Bachelor) ab 1–3 (nicht prüfbar)
Informatik allgemein (Diplom) ab 5–9

Date, Time, and Place of Course:
Mi, 14:15–15:45 (MI 01.09.014 (Church))

Date, Time, and Course of Excercise Course:
Fr, 13:00–13:45 (MI 00.09.055)

Start of Course: 26th of October 2005

Start of Excercise Course: 4th of November 2005

Expected participants: Students with Vordiplom or bachelor in computer science

Requisites: Course on Nichtsequentielle Systeme und nebenläufige Prozesse held by Prof. Veith would be helpful

Exam: The course is passed, if an exam is passed held at the end of the course.


  • Model Checking Finite Transition Systems
  • Model Checking and Abstraction
  • Parallel Model Checking
  • Model Checking Realtime Systems
  • Model Checking Probabilistic Systems