en | de

Introduction to Model Checking

master program

VO1  WS 2008/2009  703503

News

Mar 23: Results and solution of third exam online
.. on the evaluation page.
Feb 4: Results and solution of second exam online
.. on the evaluation page.
Jan 23: Date of third exam will be March 13, 8:45-9:45
Jan 21: Second exam and preliminary results online
.. on the evaluation page. Moreover, there are informations about reviewing the corrected exams.
Nov 26: Results and solution of first exam online
.. on the evaluation page.
Nov 24: First exam and preliminary results online
.. on the evaluation page. Moreover, there are informations about reviewing the corrected exams.
Nov 19: Error in blackboard-presentation
Concerning the example on Slide 26 of Chapter 4 about the CTL* model checking algorithm: Sat(E ¬(G F serve ∧ G E F main)) is {1,2,3,4,5} and not {2,4} as written down on the blackboard. Consequently, Sat(¬E ¬(G F serve ∧ G E F main)) = {6,7}
Nov 6: Final exercisess are available
.. on the exercise page.
Nov 5: Minor changes in Chapter 5
There have been minor changes in the slides of Chapter 5. The most important one is a bugfix on Slide 28. It should read: x=2 : ac2 ! ack. Moreover, the former slide 49 has been dropped, such that the new version has only 52 slides.
Oct 21: Chapter 4 is available
... on the scheduling page.
Oct 16: Solution to 1(f)
G (red ⇒ (¬orange ∧ ¬green)) ∧ G (orange ⇒ (¬red ∧ ¬green)) ∧ G (green ⇒ (¬red ∧ ¬orange)) ∧ red ∧ G (red ⇒ red U (orange ∧ orange U (green ∧ green U (orange ∧ orange U red))))
Oct 16: Date of first and second exam fixed
Details on the evaluation page.
Oct 8: New exercises are available
.. on the exercise page.
Oct 8: Change in time
From now on the lecture starts at 12:30 instead of 12:15.
Oct 8: Correction in slides of Chapter 3
There have been typos on Slides 12 and 29 which are now fixed.
Oct 6: Chapter 3 is now completed
.. and there have been minor changes in comparison to the incomplete part, e.g., true is now an LTL-primitive and not just an abbreviation).
Oct 2: Exercises are now available
.. on the new exercise page.
Oct 1: Correction in slides of Chapter 1
There was a small typo on slide 29. The correct version of line 607 must be:
607: proc 2 (Dec) line 5 "pan_in" (state 2) [((x > 0))]
On the scheduling page only the corrected versions of the slides are available.
Oct 1: Slides of Chapter 1 and 2 are available
... and should be printed out for the first lecture. The slides of Chapter 3 are already partially available.
Jun 18: News system
This is the entry-site for the Introduction to Model Checking lecture. Check this website regularly for news. For anonymous comments you can use the feedback page. If you have any question, do not hesitate to write me an email, or to visit my office. To access the slides which are used in the lecture, visit the schedule page.