**Teacher**Paolo Baldan

Dipartment of Mathematics, University of Padua

paolo.baldan[at]math.unipd.it

INF/01

**Aim**

Concurrency is pervasive in modern computing systems due to the success of mobile computing and network applications, and, at a lower level, of multicore and multiprocessor systems. The course is intended to provide a gentle introduction to the main concepts underlying the theory of concurrency and its impact on the design of languages for concurrent and distributed programming. We start by illustrating some formal modelling languages for concurrency (e.g., the Calculus of Communicating Systems) and the associated reasoning and automated verification techniques. Additionally, logical specification languages are presented and used for analysing properties of interest in a concurrent setting (including classical properties like deadlock freeness, mutual exclusion, fairness, etc.). We finally discuss the import of this theory on the design of languages with modern concurrency primitives like Google Go or Elixir/Erlang.

**Syllabus**

- Specification languages for concurrency: Milner’s Calculus of Communicating Systems

- Process equivalence and logics for the specification of system properties

- Tools for automated verification

- Google Go and channel based concurrency

- Elixir/Erlang, for massive and distributed concurrency

**Course requirements**

Some experience in programming and some basic knowledge of concurrency are useful to fully appreciate the course

**Examination modality**

None

**Schedule**

-17 Jul, 9:30 - 12:00, Room 1BC/50 at the Dept of Mathematics

-19 Jul, 9:30 - 12:00, Room 1BC/50 at the Dept of Mathematics

**Location**

To be defined