In un campo in continua e veloce evoluzione come quello del software non è da tutti realizzare un lavoro scientifico dirompente a livello internazionale e così lungimirante da influenzare il settore per gli anni a venire.
Ci è riuscito Alessandro Cimatti, del Centro ICT della Fondazione Bruno Kessler, che ieri a Uppsala in Svezia ha ricevuto il premio “Test of Time Award” dall’ ETAPS, l’’organizzazione delle conferenze europee sulla teoria e la pratica del software.
Il suo lavoro scientifico “Symbolic model-checking without BDDs” realizzato nel 1999 con il gruppo del prof. Edmund Clarke della Carnegie Mellon University è stato scelto fra gli oltre mille pubblicati nell’ambito delle conferenze ETAPS fino al 2007, il periodo preso in considerazione per la selezione di quest’anno, e insignito del premio dedicato agli articoli in grado di resistere alla prova del tempo.
Lo studio ha riguardato la realizzazione del cosiddetto Bounded Model Checking, un algoritmo che ora è utilizzato in ogni sistema di progettazione di circuiti elettronici e software. In particolare serve per analizzare in modo automatico gli eventuali errori di progettazione - prima della realizzazione del circuito stesso - così da poterli correggere per tempo assicurando maggiore velocità e risparmio di denaro. A dimostrazione della grande influenza avuta, l’articolo originale e le sue successive evoluzioni sono stati finora citati oltre 3.800 volte nei lavori scientifici di settore.
“Spesso”, afferma Cimatti, “si ottengono risultati sorprendenti combinando idee da vari settori disciplinari. Il lavoro è nato prendendo ispirazione dal campo dell’Intelligenza Artificiale, in particolare della Pianificazione, e ha prodotto una tecnica altamente innovativa nell’ambito della verifica dei sistemi digitali. Il Bounded Model Checking ha aperto la strada all’analisi di programmi e circuiti che erano semplicemente fuori dalla portata delle tecniche al momento disponibili.”
Cimatti, che ha recentemente ricevuto la abilitazione come professore ordinario nei settori disciplinari di Informatica e di Sistemi per l’Elaborazione dell’Informazione, è dal 2007 responsabile dell’unità di ricerca Embedded Systems (ES) nel centro ICT della Fondazione Bruno Kessler.
L’Unità sviluppa vari software per la verifica formale in cui il Bounded Model Checking è una parte integrante. La verifica formale viene applicata in molteplici progetti di trasferimento tecnologico, in settori critici quali l’aerospaziale, il ferroviario, il controllo avanzato e l’Industry 4.0.
