Einführung in Model Checking

.. on the evaluation page.

.. on the evaluation page.

.. on the evaluation page. Moreover, there are informations about reviewing the corrected exams.

.. on the evaluation page.

.. on the evaluation page. Moreover, there are informations about reviewing the corrected exams.

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}

.. on the exercise page.

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.

... on the scheduling page.

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))))

Details on the evaluation page.

.. on the exercise page.

From now on the lecture starts at 12:30 instead of 12:15.

There have been typos on Slides 12 and 29 which are now fixed.

.. 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).

.. on the new exercise page.

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.

... and should be printed out for the first lecture. The slides of Chapter 3 are already partially available.

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.