en | de

Introduction to Model Checking

master program

VO1  WS 2007/2008  703503


Apr 30: Solution and results of third exam online...
... on the evaluation page.
Apr 29: 3rd exam is corrected, reviewing Apr 30, 8:00-8:30, 9:00-10:00. Further details
... on the evaluation page.
Feb 28: Solution and results of second exam online...
... on the evaluation page.
Feb 20: Updated slides of lectures 8 and 9 available
There was a typo in the translation from LTL to GNBAs. The transition from q0 has input vector (d1,...,dn) and not the vector (a1,...,an).
Jan 30: Diskussion opportunity
On February 19 there will be an open discussion in HS 10 starting at 12:00. Please prepare for the second exam before and your open questions will hopefully be answered during this discussion.
Jan 30: First exam and results online...
... on the evaluation page
Jan 25: Updated slides of lectures 7 and 8 available
There was a typo in the definition of the semantics of until. The forall-quantifier for i was missing.
Jan 21: Updated slides of lecture 13 available
The slides of lecture 13 now include the channel-system for the nanoPromela graph.
Jan 15: Time of the exam is now fixed
The exam on Jan 28 will be from 13:30 - 14:30. More details are available on the evaluation page.
Jan 14: Feedback required
One part of the lecture on Jan 21 will be a short repetition of topics of your choice. To find out which topics are of most interest, please send me an e-mail with a short description of would you would like to see again until Thursday 1pm. (Send the e-mail to rene._mylastname_@uibk.ac.at or use the anonymous way via the feedback form.)
Jan 10: Updated slides of lecture 4 available
In the calculation of the size of transition graph of a promela program was a minor mistake in the example. (The local variables have not been considered.) The slides are fixed now.
Jan 02: Bugfix of Exercise 10
In the exercises of lecture 10 the ill-formed formula E A g should be replaced by E G g. The slides are updated accordingly.
Nov 12: Updated slides of lecture 6 available
The slides of lecture 6 now include the full proof that {w | w contains only finitely many A's} is not recognizable by a DBA.
Oct 15: Date of the exam
The date of the exam is fixed: Jan 28 in HS A. One can register for the exam from Nov 15 until Jan 14, 16:00.
Oct 15: Change of the lecture hall
Since HS 11 seems a little bit too small, from now on the lecture will be in HS C.
Oct 12: No registration required
Unlike what was said in the lecture, there is no registration for the lecture required! One only has to register for the exam.