E’ il prof. Luca Tesei, docente di Informatica della Scuola di Scienze e Tecnologie di Unicam, il vincitore dell’edizione 2010 del Wilkes Award, prestigioso riconoscimento che ogni anno viene assegnato al migliore articolo pubblicato nel corso dell’anno precedente dalla rivista internazionale “The Computer Journal”.

Tra i criteri per l’assegnazione del premio, stabilita da un Comitato Editoriale composto da docenti di chiara fama internazionale, ci sono l’originalità e la qualità del tema ed il modo in cui viene trattato. Il prof. Tesei è stato premiato per il suo lavoro dal titolo “An Abstract Interpretation Approach for Enhancing the Java Bytecode Verifier”, realizzato in collaborazione con i colleghi dell’Università di Pisa Roberto Barbuti e Nicoletta De Francesco, e pubblicato sul Volume 53, Issue 6 della rivista.

“Sono estremamente orgoglioso e soddisfatto – afferma il prof. Tesei – di aver ottenuto questo prestigioso riconoscimento. Il linguaggio Java è oramai diventato un linguaggio di riferimento per lo sviluppo di applicazioni software, che attualmente hanno un ampio raggio di utilizzo, dai cellulari e smartphone alle applicazioni gestionali su larga scala. La macchina virtuale Java include una componente di sicurezza chiamata verificatore del bytecode (bytecode verifier in inglese) che controlla il codice Java bytecode prima che venga eseguito. Il controllo garantisce che il codice, che potrebbe essere stato scaricato da fonti non sicure e quindi dannoso, sia invece sicuro dal punto di vista del flusso dei dati, ed esegua dunque le corrette operazioni durante l’elaborazione dei dati”.

“Il nostro lavoro – prosegue il prof. Tesei – propone un miglioramento del verificatore. Accade infatti che l’analisi eseguita risulti in alcuni casi essere troppo superficiale, per cui alcuni codici assolutamente corretti dal punto di vista del flusso dei dati vengono invece bollati come non sicuri e quindi non eseguiti. Per risolvere questo problema introduciamo una analisi astratta del codice bytecode proponendo un dominio dei tipi più ricco di quello che viene usato dal verificatore attuale. Utilizzando tecniche di interpretazione astratta proviamo matematicamente che la nostra analisi è corretta e che estende l’insieme dei programmi bytecode che sono riconosciuti corretti dal verificatore così migliorato. Ciò permette dunque l’esecuzione di programmi che prima venivano invece erroneamente bloccati”.