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

Roberta Calegari

Professoressa a contratto

Assegnista di ricerca

parole chiave: logic programming, distributed systems, service-oriented architectures, pervasive systems, intelligent systems, LPaaS,

Andrea Colledan

Dottorando

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

Ugo Dal Lago

Professore ordinario

parole chiave: Linguaggi di Programmazione, Computazione Quantistica, Crittografia, Logica nell'Informatica

Maurizio Gabbrielli

Professore ordinario

parole chiave: Linguaggi di programmazione, Constraint programming, Intelligenza aritificiale

Saverio Giallorenzo

Ricercatore in Tenure Track L. 79/2022

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

Roberto Gorrieri

Professore ordinario

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

Pietro Lami

Dottorando

Tutor didattico

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

Ivan Lanese

Professore associato

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

Cosimo Laneve

Professore ordinario

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

Simone Martini

Professore ordinario

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

Ghulam Mustafa

Dottorando

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

Claudio Sacerdoti Coen

Professore associato

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

Mirko Viroli

Professore ordinario

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