Models and languages for concurrency

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
- Abstraction, models, and specification languages for concurrency: Milner’s Calculus of Communicating Systems.
- Process equivalence and logics for the specification of system properties, with corresponding tools for automated verification
- Google Go and channel-based concurrency, Elixir/Erlang, for massive and distributed concurrency

Introductory readings
Some ideas on what the course is talk about can be grasped from the Wikipedia entries about formal methods and concurrency theory.

Course requirements
Some experience in programming and some basic knowledge of concurrency can be useful to fully appreciate the course. Depending on the background of the participants, the course could go deeper into the technical content or just present the basics, focusing instead on the concepts of (formal) model, abstraction, specification and verification of the desired properties, which can be of general interest.

Examination modality
None

Course material, enrollment and last minute notifications
Made available by the teacher at this Moodle address

Schedule
Canceled

Location
To be defined

<< Courses in 2019-2020