Obtain understanding of different methods that allow to use tools toverify the correctness of large scale concurrent and distributedsystems.
Using examples from the scientific literature, we discuss severalapproaches to verification of systems that are parametrized in thenumber of processes. Techniques discussed include networkdecomposition and counter abstraction for concurrent systems, and theCMP method that has been used for the verification of cache coherenceprotocols.
preliminary discussion on 11.03.2013; 16:00c.t., Seminar room von Neumann
ECTS-Breakdown (3 ECTS):
————————–24 hours: in class20 hours: exercises29 hours: preparation for presentation2 hours: presentation————————–75 hours: total————————–
assessment of exercises and student presentations
Not necessary
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.