Future Built on Knowledge

Alessandro Cimatti vince il premio”Test of Time Award” dell’ETAPS

aprile 27, 2017

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 a Uppsala in Svezia ha ricevuto il premio “Test of Time Award” dall’ ETAPS.

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.


Autore/i