Personale docente

Roberto Bagnara inizia la propria formazione informatica presso l'Università di Bologna (maggio 1984 - dicembre 1987) ed il CERN di Ginevra, dove ha lavorato nel gruppo di Tim Berners-Lee, inventore del World Wide Web (gennaio 1988 - luglio 1989). Ha conseguito poi presso l'Università di Pisa la laurea con lode in Scienze dell'Informazione (luglio 1992) ed il Dottorato di Ricerca in Informatica (settembre 1997). È stato Research Fellow presso la School of Computer Studies della University of Leeds (gennaio-ottobre 1997) e poi Ricercatore in Informatica presso l'Università degli Studi di Parma (novembre 1997 - dicembre 2001), Professore Associato di Informatica presso la stessa università (dicembre 2001 - ottobre 2010), dove ora è Professore Straordinario di Informatica (da novembre 2010). È stato Visiting Researcher/Professor presso la Monash University di Melbourne (gennaio-febbraio 1995), l'Université de La Réunion (vari periodi tra il 2002 ed il 2010) e l'École Polytechnique di Parigi (giugno-luglio 2008).

Dal 2000 è membro del collegio dei docenti del dottorato di ricerca in Matematica e Statistica per le Scienze Computazionali dell'Università di Milano e dal 1997 tiene corsi universitari, ad ogni livello, di fondamenti dell'informatica, linguaggi di programmazione, metodologie avanzate di programmazione, analisi e verifica del software. È stato relatore di numerose tesi di laurea e membro di commissioni di esame finale per dottorati di ricerca italiani e Ph.D. europei.

È attivo da 20 anni nei settori dell'interpretazione astratta, dell'analisi e della verifica dei sistemi software e hardware, e delle tecniche di manipolazione dei programmi basate sulla semantica.

L'interpretazione astratta è una teoria dell'approssimazione dei sistemi discreti concepita verso la fine degli anni 1970 dai francesi Patrick e Radhia Cousot. Questa teoria permette di specificare in modo formale e dimostrabilmente corretto i processi di approssimazione del comportamento di un sistema di calcolo qualsiasi. Ad esempio, l'interpretazione astratta fornisce metodi sufficientemente generali per specificare analizzatori statici di programmi, verificatori automatici di sistemi software e hardware, verificatori automatici delle proprietà dei protocolli di comunicazione, sistemi di tipo eccetera. Il campo di ricerca sull'interpretazione astratta è estremamente vivace: International Static Analysis Symposium (SAS) e International Conference on Verification, Model Checking and Abstract Interpretaton (VMCAI) sono le conferenze annuali specifiche del settore, ma numerosi contributi vengono presentati anche a International Conference on Computer Aided Verification (CAV), ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) ed altre conferenze. La comunità di ricercatori è piuttosto ampia, specialmente in Europa (ed in particolare in Italia, come testimoniato dai numerosi progetti PRIN su tematiche di interpretazione astratta), negli Stati Uniti e in Asia. L'interpretazione astratta sta avendo un notevole impatto industriale a causa della necessità imprescindibile di garantire la sicurezza del software critico. Ad esempio, l'analizzatore statico PolySpace per programmi C, C++ e Ada è interamente concepito e progettato mediante interpretazione astratta ed è un prodotto commercializzato con grande successo dalla multinazionale TheMathWorks. L'ambiente di sviluppo Microsoft Visual Studio integra un modulo di analisi statica di bytecode .NET per l'inferenza automatica di specifiche di correttezza (i cosiddetti Code Contracts). Infine, ma la lista potrebbe continuare, possiamo citare l'analizzatore statico ASTRÉE, sviluppato dal gruppo di ricerca di Patrick e Radhia Cousot, commercializzato dalla società tedesca AbsInt, e usato dal consorzio Airbus nell'ambito della certificazione del software critico di bordo per gli aerei Airbus A340 e A380.

Roberto Bagnara è coautore di circa 40 pubblicazioni sui temi suddetti in riviste e atti di conferenze internazionali con revisione. In particolare, i risultati conseguiti insieme ai suoi coautori riguardano:

• la programmazione logica e con vincoli, sia come oggetto che come strumento per l'analisi e la verifica dei programmi;
  
• l'uso in interpretazione astratta di tecniche di propagazione di vincoli precedentemente confinate al campo dell'intelligenza artificiale;
  
• l'analisi di aliasing e sharing delle variabili in programmazione logica;
  
• la semplificazione per l'analisi di pair-sharing del dominio di Jacobs e Langen;
  
• la generalizzazione di questo dominio al caso dell'assenza di occur-check, la sua combinazione con domini di freeness e linearità delle variabili, la definizione di operatori di widening sui domini combinati per accelerare la convergenza dell'analisi;
  
• la decomposizione di domini attraverso quozienti e complementazione;
  
• l'analisi della struttura dei termini in programmi logici con vincoli, con o senza occur-check;
  
• la prima analisi di finitezza per linguaggi logici (con vincoli) basati sulla teoria degli alberi razionali;
  
• la generalizzazione ai poliedri convessi non necessariamente chiusi del metodo della doppia descrizione (introdotto da Motzkin e colleghi), in modo completamente indipendente dalla particolare tecnica di implementazione utilizzata;
  
• la generalizzazione della tecnica di Halbwachs e colleghi per l'implementazione dei poliedri non necessariamente chiusi basata su epsilon-rappresentazioni;
  
• la definizione di uno schema generale per la definizione di nuovi operatori di widening sul dominio dei poliedri convessi (generalizzabile ad altri domini) mediante il quale una o più euristiche di approssimazione possono essere sistematicamente trasformate in operatori di widening più precisi del widening standard definito da Cousot e Halbwachs; prima di questo lavoro, e per 25 anni, il widening standard era l'unico operatore di widening noto sul dominio dei poliedri convessi;
  
• l'introduzione di tecniche per il "lifting" degli operatori di widening a domini astratti ottenuti per mezzo della costruzione finite powerset (la quale consente di rappresentare tutte le disgiunzioni finite di elementi del dominio astratto di partenza);
  
• la risoluzione dei problemi dovuti alla definizione "sintattica" dei domini debolmente relazionali (come i sistemi di differenze vincolate o i cosiddetti "ottagoni") passando a definizioni "semantiche" esenti da ridondanze e da problemi di convergenza, e con interfacce assolutamente intuitive;
  
• nuovi domini astratti per la generazione di invarianti espresse da congiunzioni di disuguaglianze polinomiali (di grado limitato) o costituite da insiemi di punti ed iperpiani linearmente disposti su di uno spazio vettoriale n-dimensionale (griglie razionali);
  
• un nuovo algoritmo cubico per la chiusura per entailment di insiemi di vincoli "ottagonali" interi (gli algoritmi precedentemente noti erano sia asintoticamente più complessi che meno efficienti anche su piccole istanze);
  
• la definizione di un framework per l'analisi statica basata su interpretazione astratta di linguaggi imperativi come C, C++ e Java, che supporta domini relazionali, puntatori, oggetti dato compositi e meccanismi non strutturati di controllo del flusso.
  

La ricerca di Roberto Bagnara unisce l'investigazione rigorosa dei fondamenti teorici alla validazione sperimentale e all'applicazione in contesti concreti. È stato l'ispiratore ed il principale architetto di vari progetti software negli ambiti di ricerca suddetti, tra i quali la Parma Polyhedra Library (PPL), una libreria di astrazioni numeriche specialmente concepita per applicazioni nel campo dell'analisi e della verifica di sistemi hardware e software. La PPL è utilizzata in numerosi progetti presso i più prestigiosi centri di ricerca e, in particolare, è impiegata in GCC (GNU Compiler Collection, la suite di compilatori più utilizzata al mondo). È l'autore principale di China, un analizzatore statico innovativo per programmi logici con vincoli (http://www.cs.unipr.it/China/). Ha guidato anche il progetto interdisciplinare PURRS (Parma University's Recurrence Relation Solver, http://www.cs.unipr.it/purrs/). Attualmente guida il progetto ECLAIR, un'infrastruttura di qualità industriale per l'analisi, la verifica e la trasformazione di programmi imperativi: C, C++ e Java innanzitutto.

Roberto Bagnara è stato membro di comitati di programma di congressi internazionali, tra i quali i già citati SAS e VMCAI, Annual ACM Symposium on Applied Computing (SAC, Technical Track on Software Verification), International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR), International Conference on Logic Programming (ICLP). È stato anche organizzatore di workshop e summer school internazionali nonché relatore invitato in workshop internazionali e in diversi centri di ricerca nazionali ed esteri. Svolge regolarmene attività di referee per le principali riviste e le principali conferenze internazionali inerenti i suoi interessi di ricerca.

Ha partecipato a diversi progetti di ricerca nazionali ed internazionali, tra i quali: ESPRIT Basic Research Action n. 6707 ("ParForce"); COFIN'99 "Certificazione automatica di programmi mediante interpretazione astratta", COFIN'00 "Interpretazione astratta, sistemi di tipo e analisi Control-Flow", COFIN'01 "Ragionamento su aggregati e numeri a supporto della programmazione e relative verifiche".

È stato responsabile dell'unità di Parma per i progetti PRIN'02 "Verifica di sistemi reattivi basata su vincoli", PRIN'04 "AIDA - Interpretazione astratta: progettazione ed applicazioni", e PRIN'07 "AIDA2007 - Interpretazione astratta: progettazione ed applicazioni". Nell'ambito delle "Azioni Integrate Italia-Spagna", è stato il coordinatore italiano del progetto "Ambienti avanzati per lo sviluppo di programmi logici" (IT229, 2001-2002). Nell'ambito del programma ITEA (Information Technology for European Advancement), è stato responsabile dell'unita di Parma del progetto GlobalGCC (GGCC, 2006-2009), dedicato all'introduzione, nella GNU Compiler Collection, di tecniche di analisi statica globale.

Roberto Bagnara è anche chief scientist e amministratore delegato di BUGSENG srl, una società spin-off dell'Università di Parma il cui scopo è il trasferimento all'industria di sofisticate tecnologie di verifica e validazione del software.

Un CV molto più dettagliato è disponibile all'URI http://www.cs.unipr.it/~bagnara/