Obtain understanding of different methods that allow to use tools to
verify the correctness of large scale concurrent and distributed
systems.

Using examples from the scientific literature, we discuss several
approaches to verification of systems that are parametrized in the
number of processes. Techniques discussed include network
decomposition and counter abstraction for concurrent systems, and the
CMP method that has been used for the verification of cache coherence
protocols.

preliminary discussion on 11.03.2013; 16:00c.t., Seminar room von Neumann

ECTS-Breakdown (3 ECTS):

————————–
24 hours: in class
20 hours: exercises
29 hours: preparation for presentation
2 hours: presentation
————————–
75 hours: total
————————–

assessment of exercises and student presentations

You do not need a certificate for any of the preceding courses, but we will expect you to be familiar with some of the concepts taught in these courses, e.g. temporal logic, basic understanding of distributed algorithms, and proof techniques.