From Parallel SMT to Parallel Software Verification

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 oggigiorno 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 stato 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.