This advanced course addresses Master and late Bachelor students in Computer Science. Basic knowledge in concurrency theory is a prerequisite.


The course is worth 4 credit points ETCS.


This block course will address practical modelling and verification applications of concurrency theory.

Overview of the course

The course will discuss principles, languages, software tools, and real examples of concurrent systems. Emphasis is placed on practical modeling and analysis with software tools implementing the key results of concurrency theory research.


Four areas will be covered:


1. Traditional process calculi, with a fixed number of processes and value-passing features; the languages used for this area will be LOTOS and LOTOS NT


2. Mobile process calculi, where information an channel names can be exchanged; the language used for this area will applied pi-calculus, i.e. an extension of pi-calculus with data types


3. Probabilistic systems, where the behaviour exhibits random phenomena; the language will be a guarded command language extended with probabilities


4. Stochastic timed systems, where the timed behaviour is governed by random durations; the language for this part will be MODEST, a language for hard ans softly timed systems


Time and location

The course takes place as a block course. spanning from September 10 to October 12, 2012.


It combines lectures and lab excercises. The lectures are scheduled September 10-14 and October 1-5. They take place in HS 4 in E2 4.



If you would like to participate in this course, please register for it via the CMS. An explanation how to do that is here (requires Adobe Flash Player).


Dr. Hubert Garavel

FAQ (Frequently Asked Questions)


Q1: I am interested in your block course "applied concurrency theory". Can you tell me more about the contents of the course?


The main goal of the course is to make students aware and familiar of software tools for dealing with concurrency issues. Therefore, the emphasis will be put on theoretical ideas made available through software. To provide a comparison, there will be the same difference between a "concurrency theory" course and this "applied concurrency theory" course as between an algebra course and a computer algebra course: in the latter, the emphasis is not put on handling small- degree polynomials or 4x4 matrices by hand, but on using tools such as Matlab/Scilab to handle big polynomials and large matrices. This will be a computer-based, practical approach that completes the theoretical, mathematical approaches on concurrency theory given in other courses at Saarland University.


Q2: The lectures are scheduled for September 10-14 and October 1-5, the whole day or only part of the day? What will be in between? Will the course take the whole time from Septermber 10th to October 5th?


The plan is to have 5 formal lectures of nearly 3-4 hours each (3 in September 10-14, and October 1-5). This is a first estimation, and the duration of certain lectures will be extended if required by the contents. During the lecture, a small exercise will be shown and at the end of the lecture, students will receive bigger lab exercises to be prepared "at home". During these two weeks there will be also planned face-to-face moments to discuss with students who have questions. Communications with the Lecturer (by e-mail) and the Assistant will be possible during the period of the block course.


Q3: Will there be an exam?


We do not plan an traditional exam, as this would not coincide well with the goals of the course.The basis for evaluation will be the output of the lab exercises (see below). Of course, the correctness of specifications will be the first criteria, but the presentation and readability will also be considered, as formal specifications are a means to communicate between persons and groups of persons collaborating to build a real system.


Q4: How will the lab exercises look like?


The lab exercises will be real examples (taken from research or industrial problems) to be modelled using concurrent languages and to be analyzed using software tools. To the largest extent possible, each student will get different examples than other students. Each student can use either the machines of the University or his/her own machine. We plan to provide a VirtualBox virtual machine with all the software tools pre-installed, but a student will also have the possibility to install the tools by him/herself if he/she prefers.


Q5: It cannot attend certain lectures, but is it still possible for me to attend the course?


We plan to have the slides of the lectures available on the CMS. There is no overarching formal rule that would enforce a student to be present. If he/she is not, this is done at his/her own risk. In particular, if the slides of the lectures arrive late, or personal verbal communication is used as a way to pass information to the students (which usually happens in and around the lectures), this is his/her problem.