Formal Methods for Concurrent Systems

Instructor: Prof. Rocco de Nicola (Università degli Studi di Firenze).


Jul 05, 2010 10:00 AM to Jul 16, 2010 01:00 PM (Europe/Madrid / UTC200)


Edifici Ω, room S215 (floor -2), Campus Nord, UPC, Barcelona

Add event to calendar


Dates: Monday July 5  to Friday July  17
Time:  11 to  13  (every day)
Room: tba

The course is organized under the mobility program for professors in University Master degrees funded by the Spanish Ministry of Education.

The course promotes process calculi as a useful framework for the specification, verification and analysis of concurrent systems. Critical aspects of concurrent systems are related to interaction problems instead of (sequential) computation problems. Process calculi, by focusing on process interaction, can facilitate the analysis and development of concurrent programming languages and new programming paradigms. After giving the necessary background on Labelled Transition Systems (LTS) and Structural Operational Semantics (SOS), we will start the study of a simple algebras of communicating processes, and we will gradually present more and more sophisticated enrichments (tailored to value passing, distribution, mobility, encryption) together with motivation and pragmatics for their usage. We will provide also a brief introduction to modal and temporal logics and of behavioural equivalences. By using a software tool we will (TAPAs) we will show a few example of specification and verification of concurrent systems via equivalence checking and model checking.

Note: Please confirm your atendance to the LSI secretariat (