- The lectures are be given in English by Damien Zufferey and Anthony W. Lin. The tutorials are Felix Stutz.
- The dates and rooms of the lecture are:
- Lecture: Monday, 11:45 - 13:15, room 48-453.
- Lecture: Friday, 11:45 - 13:15, room 36-265.
- The first tutorial will be on Tuesday, 29 Oct, in MPI-SWS room 111.
The tutorial will cover the verification tool
*Spin*which will be used for some exercises. - There will be
**no tutorial**on 14th and 21st of January.

We will have a**substitute**tutorial session on Thursday, 23rd of January, at 1:45pm in MPI-SWS room 111. - Tutorial: We have decided with the class' participants.
The
**tutorial**takes place on**Tuesdays 8:15am**in MPI-SWS room 111.

- Exercise sheets:
- Published on this page on Mondays
- Solutions due before the following Monday at 8am
- Hand in solutions in groups of
**3 to 4 people** - Send your solutions by email to Felix Stutz in one readable pdf file (along with code if any).

- Mailing list

We will announce everything on this website but may use the following mailing list as an additional channel. It is run by MPI-IST. In particular, you are very welcome to use it to**find a group for submission**. - 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.

**Office hour**: Damien and Felix will offer an office hour from 2:00pm to 3:00pm on Monday 2nd of March in MPI-SWS 207.- Dates: The exams will be on 5 and 6 March as well as 3 April. You should have received an e-mail with your slot. Please remember to confirm it until 16 February and to register with the university.
- 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:
- Misc:
- The repository for this page is at https://github.com/dzufferey/dzufferey.github.io/tree/master/concurrency_theory_2019
- 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_2019/viewer.html?md=concurrency_theory_2019/notes/notes_1.md`).

- Misc:

- Week 1 [draft notes]
- Overview of the course [notes]
- Reminder about basic automata theoretic concepts

- Week 2 [draft notes]
- Properties and Verification
- Petri Nets
- Verification using linear programming

- Week 3 [draft notes]
- Termination and Boundedness
- Karp and Miller Tree
- "Size" of Bounded Petri Nets

- Week 4 [draft notes]
- Well-Structured Transition Systems
- Backward coverability algorithm

- Week 5 [draft notes]
- 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]
- Communicating state machines
- Turing completeness of communicating state machines with reliable FIFO channels

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

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

- Week 9 [draft notes]
- Weak (bi-) simulation
- The π‑calculus
- Variations and extensions of the π-calculus

- Week 10
- Typing communicating processes (Damien) [draft notes]
- Testing of distributed systems (Burcu) [slides]

- Week 11
- Testing of distributed systems (Burcu) [slides]
- Bulk synchronous model (Damien) [draft notes]

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

- Week 13
- Parameterized Systems (Daniel Stan) [slides]

- Week 14
- Q&A for Theory and Exercises

- Exercise 0: Using the Spin model checker. We will use this in later exercises.
- Exercises 1 solutions: ex 1-3
- Exercises 2 solutions: ex 1-2
- Exercises 3 solutions: WIP solutions
- Exercises 4 solutions: WIP solutions
- Exercises 5
*(29.11.2020) The 1st exercise has been clarified.*solutions: WIP solutions - Exercises 6 solutions: WIP solutions
- Exercises 7 solutions: WIP solutions
- Bonus exercises 1 (week 8) solutions: WIP solutions
- Exercises 8 (week 9)
*Due date updated to January 20.*solutions: WIP solutions - Exercises 9 (week 10) solutions: WIP solutions
- Exercises 10 (week 11) solutions: WIP solutions
- Bonus exercises 2 (week 12) solutions: WIP solutions

- 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.