Ecole Polytechnique Fédérale de Lausanne
Concurrency Semantics 2005

The newsgroup of the course is located at epfl.ic.cours.cs (interface web).

  • Updated the project schedule.
  • Updated the project literature & schedule.
  • More info added. Schedule revised.
  • More info added.
  • Pages initialized.
Week Documents
2 Slides 9 on 1
3 Course notes (ps.gz), Exercises (ps.gz)
4 Course notes (ps.gz), Exercises (ps.gz)
5 Course notes (ps.gz), Exercises (ps.gz)
6 Course notes (ps.gz), Exercises (ps.gz)
7 Course notes (ps.gz), Exercises (ps.gz)
8 Course notes (ps.gz), Exercises (ps.gz)
9 Course notes (ps.gz), Exercises (ps.gz)
Exercise skeleton
ABC home page (Source code, ocaml, user's guide (ps))
10 Formal Molecular Biology Handout, Slides.
11 Transactional Memories Handout. Slides, 4on1

Professor: Uwe Nestmann
Assistant: Johannes Borgström

Course: Wednesday 13:15-15:00, room BC3
Exercises: Wednesday 15:15-17:00, room BC3

This course aims to teach mathematical foundations to understand models of concurrent programs and reactive systems. We will cover basic techniques to describe the form and meaning of program terms and to reason about them. These techniques are applied in the discussion of CCS, a well-known calculus for reactive systems, and its most prominent extension for mobile processes, the pi-calculus. Based on these calculi, we will discuss notions of equivalence for concurrent programs, as well as proof techniques to show equivalence or refinement. The course will be accompanied by pencil-and-paper as well as computer-aided verification exercises.
This course aims to strengthen both your analytical (mathematical) skills, as well as your presentation skills.

The course will be divided into two parts, one traditional ex-cathedra course accompanied with exercises (Week 3-9), and another one for projects (Week 10-13), leaving the last session for some some digression into further research topics.

  1. We will provide some course notes in various formats, accessible per session via the schedule below. Most of the development of the material will be done on the blackboard, though. The main textbook is but we will also occasionally refer to material form

  2. Working on a project essentially amounts to
    • work in a group of 3 or 4 students
    • study a particular field of application on the basis of a number of research articles
    • present in class either representative proofs or extended not too trivial case studies that use and apply (adaptations of) the techniques acquired during the course.
    • prepare a handout for the other participants of the class.

    You are welcome to suggest own projects ... but I propose the following:

Grades will be given on the following distribution of points achievable:

formal presentation (~45min per candidate) in class (with printed handout)
individual oral exam (~15min per candidate) after the semester, including the material of the projects
presence in most of the course/exercice sessions and all of the project presentations
individual informal presentation in exercice session with on-the-fly selection

Week 1 (March 9):
  • cancelled due to illness
Week 2 (March 16):
  • introduction (Slides-9on1)
  • some basic discrete mathematics (sets, relations, functions, orders, equivalences, proofs, induction)
  • brief repetition on automata and language equivalence
Week 3 (March 23):
  • transition systems and notions of equivalence
  • sequential processes and bisimulation
Easter break (March 30):
  • ...
Week 4 (April 6):
  • concurrent processes and bisimulation
Week 5 (April 13):
  • (structural) congruence and reaction
Week 6 (April 20):
  • weak bisimulation: observation equivalence
Week 7 (April 27):
  • mobility!
Week 8 (May 4):
  • basics of mobile processes
Week 9 (May 11):
  • reasoning about mobile processes
Week 10 (May 18):
  • Project presentation 1: formal molecular biology I (Caffaro, Pellet)
Week 11 (May 25):
  • Project presentation 2: transactions (Arsever, Perez)
Week 12 (June 1):
  • Project presentation 3: implementation & language design (Maye, Théoduloz)
Week 13 (June 8):
  • Project presentation 4: business process modeling (Kang, Calico)
Week 14 (June 15):
  • Project presentation :5 formal molecular biology II (Rosalez, Torruella)

Verification tools
Selected research papers
Programming languages