La prima parte introdurrà i principali metodi per definire la semantica denotazionale e operazionale di linguaggi sequenziali, la seconda introdurrà alcuni formalismi per specificare, progettare e implementare sistemi concorrenti e distribuiti, e per analizzare e verificare loro proprietà.

Programma - Richiami di programmazione sequenziale e concorrente, di matematica discreta e di tecniche di prova. Automi a stati finiti e sistemi di transizione etichettati. Semantica operazionale e denotazionale dei linguaggi di programmazione. Algebre e calcoli di processo e loro modelli come sistemi di transizione. Equivalenze comportamentali come strumenti di astrazione e minimizzazione di sistemi e come base per prove di correttezza. Logiche modali e logiche temporali, e tecniche di verifica di proprietà dei sistemi basate sul model checking.

Obiettivi Formativi - Lo studente imparerà a comprendere la semantica dei linguaggi di programmazione e a progettare e realizzare semplici sistemi concorrenti. Lo studente acquisirà le competenze necessarie a utilizzare metodi formali per la validazione di sistemi informatici, possibilmente anche attraverso strumenti software di supporto, ed acquisirà le basi per l'ulteriore studio e la ricerca su teoria dei sistemi distribuiti, dei sistemi real-time e dei sistemi fault-tolerant.