Formal Methods for Concurrent Systems
Instructor: Prof. Rocco de Nicola (Università degli Studi di Firenze).
- https://computing.phd.upc.edu/en/events/copy_of_course-on-approximation-algorithms-for-hard-combinatorial-problems-and-games
- Formal Methods for Concurrent Systems
- 2010-07-05T10:00:00+02:00
- 2010-07-16T13:00:00+02:00
- Instructor: Prof. Rocco de Nicola (Università degli Studi di Firenze).
When
Jul 05, 2010 10:00 AM to Jul 16, 2010 01:00 PM (Europe/Madrid / UTC200)
Where
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.
Abstract:
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 (merce@lsi.upc.edu)
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.
Abstract:
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 (merce@lsi.upc.edu)
Share: