Teoria della concorrenza
Programma dell'insegnamento - Corso di laurea in Informatica Magistrale internazionale
Docente
Prof. Marino Miculan
Indirizzo email
Indirizzo Pagina Web Personale
http://www.dimi.uniud.it/members/marino.miculan/
Crediti
6 CFU
Finalità
Scopo del corso è fornire le basi teoriche e le tecniche fondamentali per la definizione e lo studio della semantica dei linguaggi di programmazione contenenti gli aspetti di comunicazione, sicurezza e mobilità tipiche della computazione globale.
Allo scopo vengono presentati una serie di modelli di programmazione con differenti caratteristiche e differenti livelli di complessità. Per ciascun linguaggio vengono definite le appropriate semantiche e gli strumenti formali per la loro applicazione alla verifica di proprietà dei sistemi.
Programma
- Modelli formali per sistemi concorrenti a topologia dinamica: il π-calcolo. Sintassi, semantica operazionale late e early, bisimulazioni late, early, open. Cenni a Pict.
- Modelli per la sicurezza: lo spi-calcolo. Sintassi, semantica operazionale, verifica di proprietà di sicurezza mediante bisimulazioni. Il tool ProVerif.
- Modelli per la mobilità: il calcolo degli ambienti mobili. Sintassi, semantica operazionale, logica modale spaziale, sistemi di tipi. Varianti e applicazioni.
- Metamodelli per i sistemi concorrenti e distribuiti: i bigrafi.
Bibliografia
- Luca Aceto, Anna Ingólfsdóttir, Kim Guldstrand Larsen, Jiri Srba. Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, 2007.
- Articoli e dispense dei docenti
Modalità d'esame
Approfondimento scritto e orale su un argomento del corso.