Lead
Prof. Natasha Sharygina, Universita della Svizzera ItalianaSfruttare la paralellizzazione per la verifica dei sistemi informatici

Lay summary
I sistemi informatici occupano un posto centrale nella società moderna: la
stragrande maggioranza delle industrie di oggi dipende fortemente da
essi sia direttamente, in quanto componenti hardware o software sono i
prodotti stessi dell'azienda, che indirettamente, utilizzandoli nel 
processo di produzione del prodotto finale. La sicurezza, i costi e
l'efficienza energetica in ambiti eterogenei quali, ad esempio, quello energetico,
medico e del trasporto pubblico, dipendono sempre più dal corretto
funzionamento dei sistemi informatici. L'importanza del software nella
società implica che le conseguenze di errori al suo interno potrebbero
portare a scenari catastrofici. Dimostrare la correttezza di un
programma risulta essere, quindi, uno dei problemi centrali
dell'informatica, a tal punto che esperti del settore sono stati
premiati con il prestigioso premio Turing.

Verificare la correttezza di sistemi software è un processo complesso
richiedente una grande quantità di risorse. Noi proponiamo di
affrontare questo problema sfruttando un framework per model-checking
(questo il nome tecnico delle procedure per la verifica dei sistemi
informatici) parallelo in grado di sfruttare l'enorme potenza di calcolo
offerta oggiorno dai sistemi cloud. Questo framework verrà utilizzato per studiare la
miglior soluzione per parallelizzare diverse componenti delle tecniche di
model-checking, tra le quali vi sono i risolutori SMT, strumenti
utilizzati nell'ambito del ragionamento automatico, algoritmi di verifica, ed
altre correlate tecniche di verifica come ad esempio l'interpolazione.
I risultati di questi studi verranno applicati in due scenari
principali: risolutori SMT paralleli e algoritmi di model-checking
paralleli. Prevediamo che questi studi migliorino lo stado dell'arte
odierno non solo nell'ambito della verifica, ma anche in altri domini
applicativi dove gli strumenti per il ragionamento automatico hanno
avuto successo.