Teachers	Fabrizio Montesi https://fabriziomontesi.com/ (course responsible) Marco Peressotti https://marcoperessotti.com/ (Assistant)
Period	Fall 2019
ECTS	10 credits
Code	DM861 (https://odin.sdu.dk/sitecore/index.php?a=searchfagbesk&internkode=dm861&lang=en)
Office hours	Open door.

Summary

Multi-core processors, cloud computing, and web services make concurrent systems widespread. However, designing and programming such systems correctly is challenging, since it requires predicting how multiple programs executed independently will interact. This course aims at presenting and investigating models, reasoning techniques, and abstract programming disciplines for concurrent systems. These tools allow for translating concrete requirements and designs into precise mathematical definitions, which can be used to prove that the desired properties are provided (such as lack of deadlocks or safe usage of asynchronous channels).

Many of the models covered in the course are the bases of recent or emerging programming languages and design tools, such as BPMN, Go, and Jolie.

In relation to the competence profile of the degree it is the explicit focus of the course to:

• Give the competence to: plan and carry out scientific projects at a high professional level, including managing work and development situations that are complex, unpredictable, and require new solution.
• Give skills to: describe, analyse, and solve advanced computational problems using the learned models; develop new variants of the methods learned.
• Give knowledge and understanding of: a variety of specialized models and methods developed in computer science, based on the highest international research, including topics from the subject's research front; a scientific basis to reflect on the subject area and to identify scientific issues.

At the end of this course, the student is expected to have the following competences:

• represent real-world concurrent systems in the abstract models covered in the course;
• identify and formalise typical useful properties of concurrent systems, like deadlock-freedom and communication safety;
• prove properties of concurrent systems;
• prove general properties of formal models for concurrency.

Selected topics

• Process models for concurrency, including: CCS, pi-calculus and some of its variants.
• High-level programming languages for concurrent systems.
• Type systems for concurrency, including: types for process calculi, choreography-based type systems.
• Choreographies: languages, types, compilation, and synthesis.