Course directors: Roberto Amadio and Catuscia Palamidessi
Roberto Amadio (12h)
Daniele Varacca (12h)
Kostas Chatzikokolakis (12h)
Frank Valencia (12h)
This course introduces formal methods for reasoning about properties of concurrent systems.
Starting from 2013-2014, the second part of the course changes every year.
This year we cover methods to reason about probabilities and expressiveness in concurrent systems.
In 2014-2015 we plan to cover applications of directed algebraic topology to concurrency.
The course is organised in 20 lectures.
The course is `breakable'. This means that you get 3 credits if you pass only the first part (up to the mid-term exam) or the second part (after the mid-term) and
6 credits if you pass both. Notice that the grade we consider to give 6 credits is the average of the grades of the first and second part. For instance, if your grade is
12/20 in one part and 8/20 in the other you get 6 credits.
Shared memory models of concurrent systems (Amadio, 12h)
A shared variable parallel language.
Compositional trace model.
Denotational presentation of the trace model.
Implementing atomicity.
Rely-guarantee reasoning.
Concurrent objects.
CCS and the pi-calculus (Varacca, 12h)
Labelled transition systems. Bisimulation. Proof techniques.
The trace-bisimulation spectrum and the related modal logics
CCS a calculus of communicating systems. Characterisation of labelled bisimulation.
The pi-calculus.
Functions as processes: compiling lambda into pi.
Probabilistic models and applications (Chatzikokolakis, 12h)
Probabilistic asyncronous pi calculus
Semantics based on simple probabilistic automata
Probabilistic bisimulation (maybe also testing equivalence)
Introduction to probabilistic model checking and PRISM
Verification of anonymity protocols: Dining Cryptographers, Crowds
Expressive power of concurrent models (Valencia, 12h)
Expressiveness in Concurrency: Techniques and Criteria.
The Expressiveness of Iteration, Recursion and Name Scoping in CCS-based Calculi.
Expressiveness in the pi-Calculus: Polyadic vs Monadic Communication.
Expressiveness in the pi-Calculus: Asynchronous vs Synchronous Communication.
Expressive fragments of the pi-calculus.
The Expressiveness of Shared-Memory Communication.
Lectures are given either in French or in English depending on the teacher.
The lecture notes and the text of the examinations are in English.
The students may answer in French or English.
Lecture notes and home assignment for the first period are available
here
Semantics (2.1, 2.2, 2.4), Concurrent algorithms (2.18.2, 2.18.3), Concurrent programming (2.23.1, 2.37.1).
It is useful, though not strictly necessary, to have attended the courses 1-15 (Semantics) and 1-16 (Concurrency).
R. Amadio | Univ. Paris Diderot | PPS |
K. Chatzikokolakis | INRIA | LIX |
E. Goubault | CEA | LIST Saclay |
E. Haucourt | CEA | LIST Saclay |
J.-J. Lévy | INRIA | Rocquencourt |
J. Leifer | INRIA | Rocquencourt |
C. Palamidessi | INRIA | LIX |
F. Valencia | CNRS | LIX |
D. Varacca | Univ. Paris Diderot | PPS |
Date | Speaker | |
20 Sep | Amadio | |
27 Sep | Amadio | |
4 Oct | Amadio | |
11 Oct | Amadio | |
18 Oct | Amadio | |
25 Oct | Varacca: LTS, simulation, bisimulation, Hennessy-Milner Logic (Lecture Notes, sections 7.1,7.2,8.1) | |
1 Nov | Holidays | |
8 Nov | Varacca: mu-calculus, CCS, weak bisimulation (Lecture Notes, sections 8.2, 9.1,9.2, 7.3) | |
15 Nov | Varacca: reduction semantics, value passing, pi and LTS for pi (Lecture Notes, sections 9.3,9.4, 13.1 + SLIDES ) | |
22 Nov | Varacca: Up-to techniques, some notion of typing, encoding functions (beginning) (7.4, 13.2,13.3,14 + SLIDES ) | |
29 Nov | Varacca: Encoding functions (ending), exercices (14) | |
6 Dec | Deadline home assignment (Amadio) + Mid-term exam (Varacca) | |
13 Dec | Chatzikokolakis slides | |
20 Dec | Chatzikokolakis slides | |
10 Jan | Chatzikokolakis slides | |
17 Jan | Chatzikokolakis slides | |
24 Jan | Chatzikokolakis slides, prism files | |
31 Jan | Valencia handouts relative expressiveness | |
7 Feb | Valencia handouts absolute expressiveness | |
14 Feb | Valencia handouts expressiveness of asynchronous communication | |
21 Feb | Valencia handouts expressiveness of shared-memory and spatial communication (ECCP) | |
28 Feb | Valencia handouts expressiveness of spatial communication (Ambients) | |
| Valencia handouts expressiveness of higher-order communication(HOCORE) | |
| Valencia handouts pre-exam exercises | |
7 Mar | Final exam (Chatzikokolakis+Valencia) | |
Previous years
Year 2012-2013