Software Model Checking

Graduate Course - Summer Term 2006
Lehrstuhl für Informatik 2

News

26.06.2006

The results of the written exam are online.

26.06.2006

In Exercise 28 of the 9th assignment sheet, the assignment "x := x - 1" is missing at the end of the loop body (which, however, has no impact on the result of the dependence analysis). In part (c), the dependence set computed in (b) should be used as the slicing criterion. The corrected version can be found here.

16.06.2006

In Exercise 27 of the 8th assignment sheet, the safety property "NOT (pc1 = 2 AND pc2 = 2)" must read "NOT (pc1 = 3 AND pc2 = 3)". The corrected version can be found here.

08.06.2006

Two slides had to be corrected: on Slide 7.13, Example 7.8, transition l is visible wrt. the formula x > 0 (since the execution of l in a state where x = 0 makes the formula valid) but invisible wrt. x ≥ 0 (as this is a tautology).
On Slide 8.20, Example 8.5, α and δ are not independent since both are enabled in s0 but, after the execution of α, δ is not enabled in s1. The same applies to s2/s3. This can be fixed by adding δ-loops also to s1 and s3.
The corrected versions of the slides are available now.

31.05.2006

The written exam is scheduled for Tuesday, July 4th, 11:45-13:15 (time and place of the lecture). Details will follow.

02.05.2006

The lecture on May 9th will not start before 12:15.

07.04.2006

In Exercise 2 of the 1st assignment sheet some references are odd: "Example 2.5" must read "Example 2.3", whereas "Definition 2.6" has to be replaced by "Definition 2.4". The corrected version can be found here.

Schedule

Contents

This course is connected to the course Model Checking in which methods for the verification of concurrent systems are studied. Previous knowledge of the latter, however, is not required.

Transparencies

Exercises

Examination

• Hints
• Exam
• Sample solutions
• Results

Course Evaluation

• Evaluation forms (lecture, exercises)
• Evaluation reports (lecture, exercises)

Resources

• Textbooks:
  • D. Peled: Software Reliability Methods, Springer-Verlag, 2001
  • B. Bérard et al.: Systems and Software Verification - Model-Checking Techniques and Tools, Springer-Verlag, 2001
  • E. Clarke, O. Grumberg, and D. Peled: Model Checking, MIT Press, 1999
  • G.J. Holzmann: The Spin Model Checker - Primer and Reference Manual, Addison-Wesley, 2004
• Tools:
  • SPIN
  • SPIN tutorial (for beginners)
  • SPIN tutorial (for advanced users)

Credit Requirements

• Assignments and examination questions will be in English, answers can be given either in English or in German
• Admission to the examination requires at least 50% of the points in the exercises.
• Examination: written (90 mins)