Modelling and Validating Concurrent Systems


The main goal of this unit is to teach the students the development techniques that are needed for the development of concurrent programs in a realistic, general purpose setting, using advanced mainstream languages such as Erlang, Go and Rust.

By the end of this unit, students will have acquired knowledge, skills and competences that will enable them to:

  • Understand the challenges of concurrent programming and the concepts and fundamental techniques required for the development of correct applications;
  • Be able to develop standard solutions to address common challenges in this area, arguing for or showing their correctness;
  • Know how to instantiate the main design patterns for concurrent programming using state-of-the-art programming languages and handle the critical aspects of a concurrent application.

General characterization





Responsible teacher

António Maria Lobo César Alarcão Ravara, Carla Maria Gonçalves Ferreira


Weekly - 4

Total - 84

Teaching language



Available soon


Programming languages:

- Alan A. A. Donovan, Brian W. Kernighan. The Go Programming Language

- Steve Klabnik, Carol Nichols. The Rust Programming Language

- Joe Armstrong. Programming Erlang: Software for a Concurrent World

Foundations of concurrent programming:

- Robin Milner. Communicating and Mobile Systems: The Pi-Calculus

- Dave Clarke, Johan Ostlund, Ilya Sergey, and Tobias Wrigstad. Ownership Types: A Survey

- Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. RustBelt: Securing the Foundations of the Rust Programming Language

- Gul Agha. Actors: a model of concurrent computation in distributed systems

Complementary references:

- William Kennedy with Brian Ketelsen and Erik St. Martin. Go in Action

- Fred Hebert. Learn you some Erlang for great good!

Teaching method

Each week there is a two-hour lecture and a two-hour laboratory class.

Lectures include theoretical exposition, illustrated by case studies, and supported by the use of verification tools. In laboratory sessions, students solve exercises: modelling systems; specifying and verifying model’s properties.

Assessment includes two tests and two individual practical assignments. In both of the assignments, the student will have to model a concurrent system (these assessments differ on the complexity of the system being model), specify and verify a set of properties and write a report.

Conditions for approval: NE >= 9.5 and NT >= 9.5, where NE is the mean of tests grades and NT is the practical assignment grade.

Evaluation method

Evaluation of the concepts presented

3 individual oral tests. Each provides 15% of the final grade, rounded to decimal values.

Project evaluation

3 projects, developed in groups of 2 (exceptionaly 3, with explicit permition from the lectures), with individual oral defense, each worth 15% of the final grade, each grade rounded to decimal values. The grades of the members of the groups may be different, according to the defense.

Assigments evaluation

3 mini-projects, developed in groups of 2 (exceptionaly 3, with explicit permition from the lectures), each worth 5% of the final grade, each grade rounded to unit values. To the final grade count the best 2, being the grade of this component rounded to decimal values.

The course does not require frequência.

The discussions of the projects and the oral tests will be on Campus.

Subject matter

1. Concurrent programming using ownership and permissions

1.1 Models and concepts
1.2 The Rust programming language
1.3 Concurrent programming in Rust: channels and message passing; shared memory, arcs and mutexes; asynchronous event-driven programming
1.4 Tools and techniques to support message passing concurrent programming in Rust

2. Concurrent Programming using message passing
2.1 Models and concepts
2.2 The Go programming language
2.3 Concurrent programming in Go: synchronous channels; green threads (goroutines) and select; asynchrony; concurrent programming patterns
2.4 Tools and techniques to support message passing concurrent programming in Go

3. Concurrent programming using Actors
3.1 Models and concepts
3.2 The Erlang language
3.3 Concurrent programming in Erlang: processes; message passing; process design patterns (OTP); robustness (error handling, time-outs)
3.3 Tools and techniques to support concurrent programming in Erlang



Programs where the course is taught: