Il riconoscimento ha riguardato gli studi di Cimatti per la realizzazione del cosiddetto Bounded Model Checking, un algoritmo utilizzato nei sistemi di progettazione di circuiti elettronici e software. Una soluzione che serve in particolare 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. Premiati insieme a lui a Oxford altri scienziati di livello internazionale che si sono distinti in questo settore: Armin Biere, Edmund M. Clarke, Daniel Kroening, Flavio Lerda, Yunshan Zhu.
“Questo premio”, afferma Alessandro Cimatti, “mi riempie di orgoglio, dato che CAV è la conferenza più prestigiosa nel campo della verifica formale. Il lavoro sul Bounded Model Checking è un chiaro esempio del tipo di ricerca che ci piace portare avanti in FBK: risultati teorici con una forte ricaduta pratica. I nostri lavori nel settore, che sono citati in più di quattromila articoli scientifici, hanno consentito la verifica di sistemi su scala prima impensabile”.
Alessandro Cimatti dal 2007 è responsabile dell’unità di ricerca Embedded Systems (ES) nel Centro ICT della Fondazione Bruno Kessler che sviluppa vari software per la verifica formale di cui il Bounded Model Checking è una parte integrante. Svariati i campi di applicazione in molteplici progetti di trasferimento tecnologico, soprattutto per settori critici quali l’aerospaziale, il ferroviario, il controllo avanzato e l’Industry 4.0. Alla conferenza internazionale CAV Alessandro Cimatti ha finora contribuito con oltre 20 lavori scientifici e, sempre per i propri studi di rilievo internazionale in questo settore, lo scorso anno aveva ricevuto anche il premio “Test of Time Award” dell’ETAPS, l’organizzazione delle conferenze europee sulla teoria e la pratica del software.
