Metodi formali per la modellazione e l'analisi di sistemi concorrenti e distribuiti, in
particolare modelli basati su calcoli di processi e automi. Studio delle proprietà di espressività dei modelli e di tecniche di analisi basate su sistemi di tipi o equivalenze comportamentali. Queste tecniche sono applicate in particolare nei seguenti ambiti:
- Computazione reversibile: nella computazione reversibile è possibile tornare indietro a stati precedenti. Studio di meccanismi per il controllo della reversibilita', con l'obiettivo di sfruttare la reversibilità per riportare il sistema in uno stato consistente dopo un errore. Applicazione della reversibilità al debugging, in particolare di programmi scritti nel linguaggio Erlang, e alla computazione a basso consumo energetico.
- Computazione quantistica: tecniche di modellazione di protocolli quantistici, e loro analisi per garantirne proprieta' di correttezza.
- Computazioni orientate ai (micro)servizi: studio di modelli per
computazioni basate su (micro)servizi. Studio in particolare del linguaggio di programmazione Jolie, in collaborazione con
ItalianaSoftware s.r.l.
- Sessioni multiparty: studio di sistemi interattivi basati sul
concetto di sessione multiparty. Studio di linguaggi di specifica
di questi sistemi, con particolare enfasi sui sistemi con numero
variabile di partecipanti, e studio di tecniche per la
realizzazione di servizi/componenti compatibili con una specifica
data.
