Projekt

Zurück zur Übersicht

From Parallel SMT to Parallel Software Verification

Titel Englisch From Parallel SMT to Parallel Software Verification
Gesuchsteller/in Sharygina Natasha
Nummer 166288
Förderungsinstrument Projektförderung (Abt. I-III)
Forschungseinrichtung Facoltà di scienze informatiche Università della Svizzera italiana
Hochschule Università della Svizzera italiana - USI
Hauptdisziplin Informatik
Beginn/Ende 01.09.2017 - 31.08.2019
Bewilligter Betrag 365'000.00
Alle Daten anzeigen

Keywords (3)

Program analysis, Interpolation-based Model Checking, Proofs

Lay Summary (Italienisch)

Lead
Prof. Natasha Sharygina, Universita della Svizzera Italiana
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.

Direktlink auf Lay Summary Letzte Aktualisierung: 18.08.2017

Verantw. Gesuchsteller/in und weitere Gesuchstellende

Mitarbeitende

Verbundene Projekte

Nummer Titel Start Förderungsinstrument
153402 Harnessing Parallel Computing for Model Checking 01.07.2014 Projektförderung (Abt. I-III)
153402 Harnessing Parallel Computing for Model Checking 01.07.2014 Projektförderung (Abt. I-III)

Abstract

This proposal describes a request of extension to the SNF funded project #153402 on Harnessing Parallel Computing for Model Checking running now on its second year. The first year of the project resulted in a publication in SAT 2015, a premier conference in constraint solving, and the first cloud-based and multithreaded implementations of a parallel SMT solver using novel paralellization strategies and search space partitioning. The results so far confirm the viability of the ideas presented in the original proposal. We have found the experience obtained in the process extremely useful in further strengthening the continuation outlined already in the first proposal. Since the original proposal was funded only partially we have made certain adjustments to the extension, reformulating some of the goals for this proposal. Software has a central role in modern society: Almost all of todays industry depends critically on software either directly in the products or indirectly during the production, and the safety, cost-efficiency and environmentally friendliness of infrastructure, including the electric grid, public transportation, and health care, rely increasingly on correctly working software. The growing role of software in society means that the consequences of software faults can be catastrophic, and as a result proving the correctness of software is widely thought to be one of the most central challenges for computer science, the related work having been acknowledged with prestigious recognitions such as the Turing award. Verifying complex software can be extremely expensive. We propose to address the challenges of software verification with an extensive parallel model checking framework able to scale to the massive amounts of processing power offered by computing clouds. We will use the framework to study the parallelization of key aspects of model checking, including the underlying SMT solver used as a reasoning engine, model-checking algorithms, and widely applicable related technologies such as interpolation. The results of the framework will be used in two flagship applications, a parallel SMT solver, and a parallel software model checker. We expect the research to improve the current stateof-the-art not only in model checking, but also in other applications where constraint solving has been successful.