Metodi formali

La ricerca sui metodi formali sfrutta tecniche matematiche per la progettazione, realizzazione e verifica di sistemi software, usualmente ad alta complessità o con requisiti di qualità particolarmente stringenti. Questa ricerca copre un ampio spettro di attività, che vanno da studi teorici sulle proprietà fondamentali della calcolabilità e dell'interazione a dimostratori di teoremi (anche interattivi, ovvero capaci di sviluppare dimostrazioni formali e verificabili automaticamente tramite collaborazione uomo-macchina), da modelli di sistemi concorrenti a modelli con ricche teorie matematiche con cui specificare e verificare proprietà salienti dei sistemi, quali assenza di deadlock, possibilmente tramite strumenti automatici o semi-automatici.
Il gruppo rappresenta una linea di ricerca dipartimentale articolata in più unità tematiche ciascuna della quali ha un responsabile specifico.

Persone

parole chiave: Lambda calcolo, Linguaggi di programmazione quantistici, Semantica operazionale, Verifica di risorse
foto della persona

Ugo Dal Lago

Professore ordinario

parole chiave: Semantica Differenziale dei Programmi, Computazione Quantistica, Crittografia, Analisi Statica dei Programmi
foto della persona

Maurizio Gabbrielli

Professore ordinario

parole chiave: Linguaggi di programmazione, Constraint programming, Intelligenza aritificiale
foto della persona

Saverio Giallorenzo

Ricercatore in Tenure Track L. 79/2022

parole chiave: Linguaggi di Programmazione, Algebre di Processi, Tipi Sessione, Programmazione Coreografica, Microservizi,
foto della persona

Roberto Gorrieri

Professore ordinario

parole chiave: Modelli per la descrizione di sistemi concorrenti, Algebre di Processi e Reti di Petri, Sicurezza, Computazione
foto della persona

Pietro Lami

Dottorando

Tutor didattico

parole chiave: Semantica operazionale, Linguaggi reversibili, Metodi Formali, Reversibilità Computazionale
foto della persona

Ivan Lanese

Professore associato

parole chiave: Computazione quantistica, Linguaggi reversibili, Sessioni multiparty, Computazioni orientate ai servizi
foto della persona

Cosimo Laneve

Professore ordinario

parole chiave: linguaggi di programmazione, verifica statica di programmi, semantica dei linguaggi di programmazione, implementazione
foto della persona

Uzma Latif

Dottoranda

foto della persona

Simone Martini

Professore ordinario

parole chiave: Linguaggi di programmazione, Storia e filosofia dell'informatica, Didattica dell'informatica, Logica lineare
foto della persona

Andrea Omicini

Professore ordinario

parole chiave: simulazione, agenti intelligenti, linguaggi multiparadigma, sistemi autoorganizzanti, calcolo pervasivo, sistemi

Luca Padovani

Professore ordinario

parole chiave: Sistemi di tipo, Tipi comportamentali, Sistemi concorrenti e distribuiti, Algebre di processi, Verifica formale del
foto della persona

Claudio Sacerdoti Coen

Professore associato

parole chiave: Teoria dei tipi, Dimostrazione assistita, Mathematical knowledge management, Lambda-calcolo, Linguaggi di
foto della persona

Mirko Viroli

Professore ordinario

parole chiave: Linguaggi orientati agli oggetti, Sistemi multiagente, Simulazione e verifica, Coordinazione, Ingegneria del software,