Model-Checking SS 2015

News | Basic information | Content | Exercises | Slides | Links

31. July 2015

Here is the exam and a solution. The solution is more detailed than necessary.

9. July 2015

Exercise sheet #13 is online.

7. July 2015

More solutions (up to exercise sheet #9) are online.

2. July 2015

Solution for exercise sheets #2 and #4 are online.

1. July 2015

Exercise sheet #12 is online.

25. June 2015

Exercise sheet #11 is online.

19. June 2015

Exercise sheet #10 is online. DDcal will be needed to solve the second problem. Follow the link under "Links" to download the package.

10. June 2015

Exercise sheet #9 is online.

6. June 2015

Exercise sheet #8 is online.

28. May 2015:

Next wednesday (3. June) will be an exercise session. Exercise sheet #7 is online.

20. May 2015:

Slide 255 has been corrected. If a and c are both visible, then no reduction is possible.

19. May 2015:

The slides for the Part 8: Partial-Order Reduction have been improved. There are many small changes. It is recommended to print the slides for this part again.

15. May 2015:

Exercise sheet #6 is online.

8. May 2015:

Some minor corrections to the slides in the definition of the states of the Buechi automaton for a formula.

The changes are in slide 139 (definition od subformulas), slide 141 (definition of consistent set), slide 143 (definition of the accepting condition), and slide 147 (small adjustment to the proof). The new version is under "Slides".

7. May 2015:

Exercise sheet #5 is online.

30. April 2015:

Exercise sheet #4 is online.

29. April 2015:

For more details about the Needham-Schröder protocol, see this paper and this Promela model

14. April 2015:

This week there will be three theory lectures, on Tuesday, Wednesday, and Thursday. Next week there will be two exercise lectures on Tuesday and Wednesday.

Starting next week, Tuesday's lecture will start at 8:30 instead of 8:15.

04. February 2015:

Creation of the website.