First cycle
degree courses
Second cycle
degree courses
Single cycle
degree courses
School of Science
Course unit
SCM0018214, A.A. 2015/16

Information concerning the students who enrolled in A.Y. 2015/16

Information on the course unit
Degree course Second cycle degree in
SC1176, Degree course structure A.Y. 2014/15, A.Y. 2015/16
bring this page
with you
Number of ECTS credits allocated 6.0
Type of assessment Mark
Website of the academic structure
Department of reference Department of Mathematics
Mandatory attendance No
Language of instruction Italian
Single Course unit The Course unit can be attended under the option Single Course unit attendance
Optional Course unit The Course unit can be chosen as Optional Course unit

Teacher in charge PAOLO BALDAN INF/01

ECTS: details
Type Scientific-Disciplinary Sector Credits allocated
Core courses INF/01 Computer Science 6.0

Course unit organization
Period Second semester
Year 1st Year
Teaching method frontal

Type of hours Credits Teaching
Hours of
Individual study
Lecture 6.0 48 102.0 No turn

Start of activities 01/03/2016
End of activities 15/06/2016
Show course schedule 2019/20 Reg.2014 course timetable

Examination board
Examination board not defined

Prerequisites: The course requires some familiarity with basic mathematical concepts such as relations, functions, sets, cardinality, partial orders, principles of induction, deduction systems based on inference rules. Some basic knowledge of programming language semantics are useful.
There are no propaedeutical courses.
Target skills and knowledge: The widespread diffusion of concurrent, distributed and mobile systems makes the classical programming and specification paradigms inadequate and opens complex and fascinating challenges. A rethinking appears necessary, starting from the foundations and adopting a rigorous, formal and disciplined approach. The aim of the course is to introduce the student to themes of interest in the area, using as tools type systems, process calculi and modelling languages in general. Starting from topics which are by now classical (like the Calculus of Communicating Systems and pi-calculus), we will reach some advanced issues of the research in the area. Some languages that implement the theoretical developments discussed are presented, including advanced languages for concurrency (Google Go, Erlang), orchestration languages (ORC) and languages for service oriented programming (Jolie).
Examination methods: Class exercises, solution and oral discussion of some advanced exercises, presentation on a theme choosen by the student. Among the options, there is the possibility of realizing a small project using a tool for formal verification.
Assessment criteria: The student is evaluated on his ability of solving simple exercises, witnessing the acquisition of the notions and techniques exposed in the course. Some advanced exercises test the ability of using the acquired expertise in the solution of new problems. The presentation verifies the capability of the student of deepening, autonomously, research themes in the area of interest and of properly exposing what she learnt.
Course unit contents: The structure and themes of the course will be as follows:

- Introduction to concurrency and mobility: from automata to reactive and concurrent systems.

- Calculus of Communicating Systems (CCS), a basic language for the description of concurrent systems. Process equivalence: transition systems and bisimulation.

- Hennessy-Milner logic and tools for verification. Mutual exclusion, deadlock freeness, fairness. Safety and liveness properties.

- Verification of properties with automated tools. The Concurrency Workbench and the Mobility Workbench.

- Systems with dynamic topology and mobility: pi-calculus. Specification of spatial properties and applications to protocol security.

- From specification languages ​​to programming languages​​: advanced languages ​​for concurrency (Google Go, Erlang), orchestration languages ​​(ORC) and languages for service-oriented programming ​​(Jolie).
Planned learning activities and teaching methods: Lectures and use of tools for automatic verification.
Additional notes about suggested reading: The textbook is complemented with research papers and online resources.
Web page:
Textbooks (and optional supplementary readings)
  • R. Milner, Communication and Concurrency. --: Prentice Hall, 1989. Testo di consultazione, disponibile in biblioteca Cerca nel catalogo
  • L. Aceto, A. Ingolfsdottir, K.G. Larsen, J. Srba, Reactive systems. --: Cambridge University Press, 2007. Testo adottato, si utilizzeranno i capitoli 1-7. Cerca nel catalogo