Docente: Alberto Pettorossi. Il docente riceve dopo le lezioni e per appuntamento.

Lectures:  from 15.05.05 to 15.07.05

Obiettivo del corso.
Introduzione ai metodi di definizione della semantica dei linguaggi
di programmazione concorrente e distribuita. Introduzione ai metodi
di verifica della correttezza di programmi scritti in tali linguaggi.

Prerequisiti: Calcolo dei Predicati. Elementi di Informatica Teorica.

Programma del corso:
Guarded commands (Dijkstra). Communicating Sequential Processes (Hoare).
Pure CCS (Milner). CCS with value passing (Milner). Hennessy-Milner Logic.
The Modal mu-calculus. Local model checking. Verification of Concurrent
processes. Verification of infinite state systems (Fioravanti et al.).
Verification of security/cryptographic protocols (optional).

Modalità di esame:  Presentazione di esercizi svolti e seminario su un progetto.
Progetti:
(i) CCS e correttezza dell'algoritmo di Peterson per la mutua esclusione [2].
(ii) CCS e correttezza dell'Alternating Bit Protocol [2].
(iii) Serializzabilita` delle transazioni in Basi di Dati [2].
(iv) Algoritmi distribuiti di Termination Detection [2].
(v) Correttezza di algoritmi di mutua esclusione [3].

Testi di riferimento:
1. Winskel, G.: The Formal Semantics of Programming Languages: An Introduction,
   The MIT Press, 1993. (also available in Italian).
2. Alberto Pettorossi: Elements of Concurrent Programming. Aracne. 2004
3. Articoli scientifici .
-------------------------------------------------------------