For a Human-Centered AI

Alessandro Cimatti e Roberto Sebastiani vincono il Computer-Aided Verification Award 2021

26 Luglio 2021

I due ricercatori, rispettivamente di FBK e dell’Università di Trento, hanno ricevuto il premio conferito nell’ambito di CAV 2021, la più importante conferenza internazionale sulla verifica di correttezza di sistemi hardware e software e una delle più prestigiose in informatica.

Il riconoscimento è stato assegnato per la loro ricerca pionieristica nell’ambito della SMT (“Satisfiability Modulo Theories”), disciplina dell’Intelligenza Artificiale che punta a sviluppare algoritmi in grado di risolvere automaticamente problemi logico-matematici e che ha come applicazione principale la progettazione corretta per la costruzione di microprocessori, software e impianti ad alta criticità. In sintesi, si tratta di progettare sistemi informatici che verifichino la correttezza di altri sistemi informatici, che si utilizzano ad esempio nella verifica dei sistemi di controllo e sicurezza di veicoli come gli aerei e di dispositivi hardware.

Il premio, vinto insieme ad altri autori che a livello internazionale si sono distinti nel settore, è stato annunciato durante la conferenza, organizzata per questa edizione in modalità online, in seguito alla situazione epidemiologica in corso. La cerimonia ufficiale di consegna del premio si terrà invece nell’edizione 2022 che si svolgerà in Israele.

Alessandro Cimatti, direttore del Centro Digital Industry della Fondazione Bruno Kessler, riceve per la seconda volta il prestigioso riconoscimento, dopo essere stato premiato con il CAV Award nel corso dell’edizione 2018. Roberto Sebastiani, professore ordinario presso Dipartimento di Ingegneria e Scienza dell’Informazione (DISI) dell’Università di Trento, è autore di uno degli articoli più citati al mondo in tema di SMT. La loro collaborazione dura da oltre vent’anni: hanno scritto insieme quasi quaranta articoli scientifici, molti dei quali sono lavori fondazionali sul tema per i quali sono stati premiati; hanno dato vita al progetto MathSAT, e hanno supervisionato in modo congiunto numerosi studenti di dottorato. Un loro articolo relativo a un progetto per Intel sull’applicazione di SMT alla verifica di microprocessori era stato premiato nel 2010 alla conferenza “Formal Methods for Computer-Aided Design”.

“Le tecniche basate su SMT”, dichiara Alessandro Cimatti, “sono diventate uno dei pilastri tecnologici del Centro Digital Industry, che è all’avanguardia per quanto riguarda la verifica formale e l’analisi di sicurezza, con numerosi progetti di trasferimento industriale in ambito avionico, spaziale, ferroviario, dell’elettronica e del controllo di processo”.

“SMT”, sottolinea Roberto Sebastiani, “nacque dall’intuizione di integrare algoritmi per ragionamento logico con altri appartenenti a campi molto diversi, quali la soluzione numerica di problemi matematici o la manipolazione di sequenze di caratteri o elementi, aumentandone l’efficacia ed estendendone notevolmente i campi applicativi.”