Projekt

Zurück zur Übersicht

Harnessing Parallel Computing for Model Checking

Titel Englisch Harnessing Parallel Computing for Model Checking
Gesuchsteller/in Sharygina Natasha
Nummer 153402
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.07.2014 - 30.06.2016
Bewilligter Betrag 306'212.00
Alle Daten anzeigen

Keywords (3)

Interpolation-based Model Checking, Formal Verification, SAT/SMT

Lay Summary (Italienisch)

Lead
Prof. Natasha Sharygina, Universita della Svizzera Italiana Sfruttare 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.
Direktlink auf Lay Summary Letzte Aktualisierung: 11.07.2014

Verantw. Gesuchsteller/in und weitere Gesuchstellende

Mitarbeitende

Publikationen

Publikation
PVAIR: Partial Variable Assignment InterpolatoR
Jancik P., Alt L., Hyvarinen A., Kofron J., Sharygina N. (2016), PVAIR: Partial Variable Assignment InterpolatoR, in FASE 2016, Springer, ETAPS.
Search-Space Partitioning for Parallelizing SMT Solvers
Hyvarinen A.E.J., Marescotti M., Sharygina N. (2015), Search-Space Partitioning for Parallelizing SMT Solvers, in SAT 2015, Springer, SAT15 conference.
A Proof-Sensitive Approach for Small Propositional Interpolants
Alt Leonardo, Fedyukovich Grigory, Hyvarinen Antti E. J., Sharygina Natasha (2016), A Proof-Sensitive Approach for Small Propositional Interpolants, in VSTTE 2015, Springer, San Francisco.
Flexible Interpolation for Efficient Model Checking
Hyvarinen Antti E. J., Alt Leonardo, Sharygina Natasha (2016), Flexible Interpolation for Efficient Model Checking, in MEMICS 2015, Springer, Tecs.

Zusammenarbeit

Gruppe / Person Land
Felder der Zusammenarbeit
Software Engineering Institute, Carnegie Mellon University Vereinigte Staaten von Amerika (Nordamerika)
- vertiefter/weiterführender Austausch von Ansätzen, Methoden oder Resultaten
- Publikation
Programming Principles and Tools Group, Microsoft Research, Cambridge Grossbritannien und Nordirland (Europa)
- vertiefter/weiterführender Austausch von Ansätzen, Methoden oder Resultaten
- Publikation
- Austausch von Mitarbeitern

Wissenschaftliche Veranstaltungen

Aktiver Beitrag

Titel Art des Beitrags Titel des Artikels oder Beitrages Datum Ort Beteiligte Personen
MEMICS conference Vortrag im Rahmen einer Tagung Flexible Interpolation for Efficient Model Checking. 23.10.2015 Tecs, Tschechische Republik Hyvarinen Antti; Marescotti Matteo; Sharygina Natasha


Auszeichnungen

Titel Jahr
Grant from "NATO Science for Peace and Security" to attend Marktoberdorf summer school. 2015

Verbundene Projekte

Nummer Titel Start Förderungsinstrument
166288 From Parallel SMT to Parallel Software Verification 01.09.2017 Projektförderung (Abt. I-III)
166288 From Parallel SMT to Parallel Software Verification 01.09.2017 Projektförderung (Abt. I-III)

Abstract

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 increasing 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 state-of-the-art not only in model checking, but also in other applications where constraint solving has been successful.