- The lecture will be given in English by Daniel Neider and Damien Zufferey and the tutorials by Simin Oraee. Furthermore, Ivan Gavran (Last year's TA) might do a few lectures when other people are travelling.
- The dates and rooms of the lecture are:
- Lecture: Monday, 11:45 - 13:15, room 48-453.
- Lecture: Friday, 11:45 - 13:15, room 48-453.
- Tutorial: the tutorials are scheduled on Wednesday from 17:15 to 18:45 in the MPI building room 113 (Paul-Ehrlich-Str. 26, 1st floor).

- Exercise sheets:
- Published on this page on Tuesdays
- Solutions due before the following Tuesday morning
- Hand in solutions in groups up to 3 people
- Send your solutions by email to Simin Oraee in pdf, markdown, or text format (along with code if any).

- Exam:
- There will be an oral exam.
- To be admitted, you have to fulfil the following requirements:
- 60 percent of your exercises have to be marked by a plus (useful answer).
- You have to present some of your exercise solutions on the board.

- Dates: end of February / beginning of March (we will organize a poll over emails)
- We are trying to group the exams during the following two weeks: (1) Feb 25 - Mar 1 and (2) Mar 25 - Mar 29.
- If you have not already done so, please send the week you would like to participate in the exam to Damien.

- Format:
- Questions: You will pick three questions at random from a pool and keep two
- Preparation: You will have half an hour to think about the question and prepare. You will have access to the course material during that time.
- Examination: The examination will last half an hour in which you will discuss the question and we will ask further questions/clarifications.

- Misc:
- The repository for this page is at https://github.com/dzufferey/dzufferey.github.io/tree/master/concurrency_theory_2018
- The
`*.md`files are in the Markdown format with some extensions for math formula and graphs. The encoding is UTF-8 to get the math characters. Due to the extensions, it is recommended to view the files with the link below. If you want to view the notes offline you need to:- Clone the repository.
- Run a local web server in the root folder of the repository (for instance:
`python -m SimpleHTTPServer 8080`). - View the notes through a browser (
`http://127.0.0.1:8080/concurrency_theory_2018/viewer.html?md=concurrency_theory_2018/notes_1.md`).

- Week 1 [draft notes]
- Overview of the course (Daniel and Damien)
- Reminder about basic automata theoretic concepts (Daniel)

- Week 2 [draft notes] (Damien)
- Petri Nets
- Verification using linear programming

- Week 3 [draft notes] (Damien and Ivan)
- Structural properties: siphons, traps
- Boundedness
- Karp and Miller Tree

- Week 4 [draft notes] (Ivan and Daniel)
- Well-Structured Transition Systems
- Backward coverability algorithm

- Week 5 [draft notes] (Damien)
- Forward coverability algorithm (The notes have quite a lot of material. We will trim them down depending on what we have the time to cover in class.)

- Week 6 [draft notes] (Daniel)
- Communicating state machines
- Turing completeness of communicating state machines with reliable FIFO channels

- Week 7 [draft notes] (Damien)
- Lossy Channel System
- Simple regular expression and WQO for LCS

- Week 8 [draft notes] (Damien)
- LTS, Simulations and bisimulations
- Calculus of Communicating Systems (CCS)
- Structural congruence
- Expressive power of CCS

- Week 9 [draft notes] (Damien)
- Weak (bi-) simulation
- The π‑calculus

- Week 10 [draft notes] (Damien)
- Variations and extensions of the π-calculus
- Typing communicating processes

- Week 11 [draft notes] (Damien)
- Bulk synchronous model
- Analysis of bulk synchronous programs and cut-off bound

- Week 12 [draft notes] (Damien)
- Weak memory model
- TSO (Total Store Order)
- WSTS for TSO

- Week 13 (Damien)
- Recap and Context
- Q&A for Theory

- Week 14 (Damien)
- Q&A for Theory and Exercises

- Exercises 1, solutions: ex 1-3, some (in)correct variations of lock encodings in Spin ex 4 v1, ex 4 v2, ex 4 v3
- Exercises 2, solutions: ex 1-2, ex 3
- Exercises 3, solutions: ex 1-2
- Exercises 4, solutions: ex 1-2
- Exercises 5, solutions: ex 1-2
- Exercises 6, solutions: ex 1-2
- Exercises 7, solutions: ex 1-3, ex 1 spin part
- Exercises 8, solutions: ex 1-3
- Exercises 9, solutions: ex 1-3
- Exercises 10, solutions: ex 1-2
- Exercises 11, solutions: ex 1-2

- Bonus exercises 1, solutions: ex 1-3
- Bonus exercises 2, solutions: ex 1-2
- Bonus exercises 3, solutions: ex 1. The exercise about reframing subtyping as an alternating refinement/simulation relations turned out to be more complicated than expected. I suppose we can see this as an exploration of the trade-off between strong result on restricted framework and a weaker result on more general framework.

- Lecture Notes from previous years by Roland Meyer.
- Decidability and complexity of Petri net problems – an introduction by Javier Esparza.
- Free Choice Petri Nets by Jörg Desel and Javier Esparza, 1995.
- Well-Structured Transition Systems Everywhere! by Alain Finkel and Philippe Schnoebelen, 1998.
- Forward Analysis for WSTS, Part III: Karp-Miller Trees by Michael Blondin, Alain Finkel, and Jean Goubault-Larrecq, 2017.
- On Communicating Finite-State Machines by Daniel Brand and Pitro Zafiropulo, 1983.
- A Calculus of Mobile Processes Pt.1 by R. Milner, J. Parrow and D. Walker, 1992.
- A Calculus of Mobile Processes Pt.2 by R. Milner, J. Parrow and D. Walker, 1992.
- The Polyadic pi-Calculus: A Tutorial by Robin Milner, 1993.
- On the Verification Problem for Weak Memory Models by Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, Madanlal Musuvathi, 2010.
- The Benefits of Duality in Verifying Concurrent Programs under TSO by Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Tuan Phong Ngo, 2016.
- The Design and Implementation of a Verification Technique for GPU Kernels by Adam Betts, Nathan Chong, Alastair F. Donaldson, Jeroen Ketema, Shaz Qadeer, Paul Thomson, and John Wickerson, 2015.
- ...

The files available in https://github.com/dzufferey/dzufferey.github.io/tree/master/concurrency_theory_2017 are licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.