Project

Back to overview

Harnessing Parallel Computing for Model Checking

English title Harnessing Parallel Computing for Model Checking
Applicant Sharygina Natasha
Number 153402
Funding scheme Project funding (Div. I-III)
Research institution Software Institute Facoltà di scienze informa Universit`a della Svizzera italiana
Institution of higher education Università della Svizzera italiana - USI
Main discipline Information Technology
Start/End 01.07.2014 - 30.06.2016
Approved amount 306'212.00
Show all

Keywords (3)

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

Lay Summary (Italian)

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.
Direct link to Lay Summary Last update: 11.07.2014

Responsible applicant and co-applicants

Employees

Publications

Publication
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.
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.

Collaboration

Group / person Country
Types of collaboration
Software Engineering Institute, Carnegie Mellon University United States of America (North America)
- in-depth/constructive exchanges on approaches, methods or results
- Publication
Programming Principles and Tools Group, Microsoft Research, Cambridge Great Britain and Northern Ireland (Europe)
- in-depth/constructive exchanges on approaches, methods or results
- Publication
- Exchange of personnel

Scientific events

Active participation

Title Type of contribution Title of article or contribution Date Place Persons involved
MEMICS conference Talk given at a conference Flexible Interpolation for Efficient Model Checking. 23.10.2015 Tecs, Czech Republic Hyvarinen Antti; Marescotti Matteo; Sharygina Natasha;


Awards

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

Associated projects

Number Title Start Funding scheme
166288 From Parallel SMT to Parallel Software Verification 01.09.2017 Project funding (Div. I-III)
166288 From Parallel SMT to Parallel Software Verification 01.09.2017 Project funding (Div. 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.
-