Laureato in Scienze dell’Informazione nell’aprile 1991 presso l’Università di Pisa, nel febbraio 1996 consegue il titolo di dottore di ricerca in Informatica (VII Ciclo) nel consorzio formato dalle Università di Genova-Pisa-Udine con una tesi sugli approcci algebrici ai sistemi di riscrittura.
Dall’ottobre 1996 al settembre 1998 è titolare di una borsa post-dottorato presso il Politecnico (Technische Universität) di Berlino, membro del gruppo di ricerca “Theoretische Informatik – Formale Spezifikation”; dall’aprile al dicembre 1999 è research fellow presso l’Università di Edinburgo, membro del “Laboratory for the Foundations of Computer Science”.
Ricercatore universitario dal gennaio 2000 al dicembre 2004 e Professore associato dal gennaio 2005 presso il Dipartimento di Informatica dell’Università di Pisa.
Nel corso degli anni ha fatto parte di numerosi progetti italiani (PRIN) ed europei (TMR, ESPRIT, FET), e dal 2010 al 2012 è stato responsabile nazionale del PRIN SisteR (20088HXMYN) “Sistemi di Riduzione e di Transizione””.
Dal gennaio 2008 è membro di IFIP (International Federation for Information Processing) working group 1.3 “Foundations of System Specification”, dal giugno 2013 di IFIP working group 9.7 “History of Informatics” e dal 2015 della commissione scientifica del GRIN (Gruppo di Informatica).
Dal gennaio 2012 è membro del comitato esecutivo dell’Internet Festival e dal novembre 2013 è Direttore del Museo degli Strumenti per il Calcolo dell’Università di Pisa.
All’interno dell’area dei metodi formali, Il fuoco principale della ricerca sono le tecniche per la specifica e la verifica di sistemi concorrenti e distribuiti. Gli argomenti principali sono lo sviluppo di modelli operazionali e denotazionali (spesso con strumenti della teoria delle categorie), l’uso di logiche per la specifica di sistemi distribuiti e con risorse limitate, l’applicazione di tecniche dalla teoria dei grafi (e della loro riscrittura) per modellare sistemi concorrenti (specificati da calcoli di processi), e lo sviluppo di linguaggi e tecniche per la programmazione con vincoli.
