Teoria della Concorrenza

Corso biennalizzato: tace nell’A.A. 2014/15, e verrà offerto nell’A.A. 2015/16.

Docente

Prof. Marino Miculan

Crediti

6 CFU

(per la versione da 12 CFU offerta fino all’A.A. 2013/14 si veda Teoria della Concorrenza (12 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

  1. Luca Aceto, Anna Ingólfsdóttir, Kim Guldstrand Larsen, Jiri Srba. Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, 2007.
  2. (Propedeutico per chi non ha seguito un corso di logica) Michael Huth, Mark Ryan. Logic in Computer Science – Modelling and Reasoning about Systems. Cambridge University Press, 2004.
  3. Articoli e dispense indicati dal docente

A monte di ciò, può essere utile leggere una guida introduttiva a come leggere un articolo scientifico.

Modalità d’esame

Approfondimento scritto e orale su un argomento del corso, da concordare con il docente.