Personale docente

Enea Zaffanella è Professore Associato di Informatica presso l'Università degli Studi di Parma, dal novembre 2006, afferendo al Dipartimento di Matematica e Informatica. In precedenza aveva prestato servizio presso la stessa sede come assegnista di ricerca (dal giugno 2000 al dicembre 2002) e come ricercatore universitario (dal dicembre 2002 all'ottobre 2006). Dal 2002 è titolare di insegnamenti universitari presso i corsi di laurea in Informatica, Matematica e Fisica, aventi per argomento le metodologie di programmazione (sia a livello base che avanzato), le basi di dati e la compilazione dei linguaggi di programmazione, svolgendo l'attività di (co-) relatore di numerose tesi di laurea focalizzate sulla propria attività di ricerca.

Laureatosi con lode in Scienze dell'Informazione presso l'Università di Pisa nell'aprile 1993, ha proseguito la propria formazione informatica svolgendo attività di ricerca presso il Dipartimento di Informatica. Dopo avere prestato servizio dal 1997 al 2000 come laureato tecnico presso le Università di Modena e di Parma, nel 2002 ha conseguito il Dottorato di Ricerca in Informatica presso la School of Computing dell'Università di Leeds (Regno Unito), presso la quale è stato in seguito Visiting Researcher in più occasioni.

L'attività di ricerca, iniziata durante il lavoro di tesi di laurea, si inquadra nel settore dell'analisi e verifica dei sistemi software mediante interpretazione astratta. In tale ambito, assumono interesse le problematiche attinenti la specifica della semantica dei linguaggi di programmazione e lo sviluppo di tecniche formali per l'approssimazione corretta di tale semantica per infine giungere allo studio, progettazione, implementazione e valutazione sperimentale di domini ed operatori astratti in grado di supportare efficacemente il calcolo di tali approssimazioni. L'attività di ricerca svolta su tali argomenti ha portato alla pubblicazione di oltre 35 pubblicazioni in riviste e atti di conferenze internazionali con revisione.

Una prima parte dei risultati dell'attività di ricerca riguarda le problematiche attinenti l'analisi dei linguaggi di programamzione logica con vincoli, eventualmente estesi con l'utilizzo di costrutti di sincronizzazione per la specifica di programmi concorrenti. In tale ambito, particolare importanza ha rivestito lo studio dei domini per l'analisi di sharing delle variabili logiche per la quale, oltre a dimostrare in maniera rigorosa la correttezza, sono state proposte modifiche atte a migliorarne l'efficienza, la precisione e la scalabilità, anche in combinazione con analisi di freeness, linearità ed informazioni sulla struttura dei termini. I risultati ottenuti sono validi sia per un dominio di termini finiti, sia per un dominio di termini razionali, e trovano applicazione in entrambi i contesti.

Una seconda parte dell'attività di ricerca si è focalizzata sui domini per l'approssimazione delle quantità numeriche manipolate dai programmi. Per il dominio astratto dei poliedri convessi è stata formulata una elegante generalizzazione del metodo della doppia descrizione al caso dei poliedri non necessariamente chiusi, giustificandone la correttezza e confrontando l'efficienza di approcci implementativi alternativi. Per le approssimazioni debolmente relazionali (differenze vincolate ed ottagoni) è stato mostrato come l'utilizzo opportuno degli operatori di chiusura per entailment e di riduzione delle ridondanze permetta l'adozione di domini basati sul concetto di equivalenza semantica delle rappresentazioni, invece della mera equivalenza sintattica utilizzata precedentemente. Per il dominio degli ottagoni, è stato definito un operatore di chiusura per entailment più semplice e, al tempo stesso, più efficiente di quelli noti precedentemente; inoltre, sono stati definiti innovativi operatori di riduzione, sia per il caso razionale che per il caso intero. Lo studio del dominio delle griglie (sistemi di congruenze lineari) ha portato alla definizione di un insieme funzionalmente completo di operatori astratti che ne consentono l'inclusione in framework di analisi esistenti. Si è infine studiato il problema generale di individuare in quali casi l'unione di approssimazioni numeriche può essere rappresentata, senza perdita di precisione, da un elemento del dominio, fornendo algoritmi innovativi per alcuni domini di calcolo e, in particolare, un più efficiente algoritmo per il caso dei poliedri convessi.

Un'altra parte dei risultati ottenuti riguarda la definizione sistematica di operatori di widening, atti a garantire o accellerare la terminazione dell'analisi. Oltre a definire e valutare operatori specifici per alcuni domini, sono stati proposti schemi generali di costruzioni di widening: un primo schema prevede di migliorare la precisione di un operatore di widening esistente incorporando al suo interno tecniche euristiche che, prese isolatamente, non garantirebbero la convergenza dell'analisi; un secondo schema consente di definire operatori di widening su collezioni disgiuntive di elementi astratti a partire dall'operatore definito sui singoli elementi.

L'attività di ricerca svolta è stata caratterizzata dal ricorso metodico alla validazione sperimentale dei risultati teorici ottenuti. Questo approccio ha comportato una sistematica collaborazione allo sviluppo di alcuni innovativi progetti software. In particolare, la Parma Polyhedra Library (PPL), una libreria di astrazioni numeriche concepita per applicazioni di analisi e verifica di sistemi hardware e software; China, un analizzatore statico per programmi logici con vincoli; ECLAIR, un analizzatore statico preciso ed efficiente per linguaggi imperativi di uso comune, quali il C ed il C++. Molte ricerche hanno anche trovato applicazione diretta nel contesto dello spin-off universitario BUGSENG srl, presso il quale ha lavorato allo sviluppo di strumenti di analisi statica dalla sua fondazione fino al 2014.

Durante l'attività di ricerca, oltre a svolgere attività di referee per riviste e conferenze internazionali, è stato membro del comitato di programma di alcuni workshop e conferenze, nazionali ed internazionali: Joint Conference on Declarative Programming (APPIA-GULP-PRODE), Convegno Italiano di Logica Computazionale (CILC), Workshop on Logic-Based Methods in Programming Environments (WLPE), Workshop on Numerical and Symbolic Abstract Domains (NSAD), Sattic Analysis Symposium (SAS). Ha partecipato a diversi progetti di ricerca nazionali ed internazionali: 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" PRIN'02 "Verifica di sistemi reattivi basata su vincoli" PRIN'04 "AIDA - Interpretazione astratta: progettazione ed applicazioni" PRIN'07 "AIDA2007 - Interpretazione astratta: progettazione ed applicazioni" Azioni Integrate Italia-Spagna IT229 "Ambienti avanzati per lo sviluppo di programmi logici".