Project

Back to overview

Beyond Symbolic Model Checking through Deep Modelling

English title Beyond Symbolic Model Checking through Deep Modelling
Applicant Sharygina Natasha
Number 185031
Funding scheme Project funding (Div. I-III)
Research institution Istituto del Software (SI) Facoltà di scienze informatiche
Institution of higher education Università della Svizzera italiana - USI
Main discipline Mathematics
Start/End 01.11.2019 - 31.10.2023
Approved amount 950'000.00
Show all

All Disciplines (2)

Discipline
Mathematics
Information Technology

Keywords (5)

Reliable Software; Abstraction; Satisfiability Modulo Theories; Formal Verification by Model Checking; Secure Smart Contracts

Lay Summary (Italian)

Lead
Prof. Dr. Natasha Sharygina
Lay summary
La verifica formale del software, sviluppatasi conseguentemente al grande successo della verifica di sistemi hardware, sta attualmente affrontando un drastico aumento del numero di applicazioni per la sicurezza di sistemi critici, i quali sono scritti in linguaggi di programmazione concettualmente sempre più lontani da quelli usati in ambito hardware. Ad esempio, l'emergere di algoritmi di consenso distribuito su larga scala e le relative applicazioni nell'ambito degli "smart contracts" non solo ha creato nuove opportunità di ricerca, ma ha anche messo in discussione il modo in cui la verifica è attualmente effettuata, ad esempio, in presenza di stringhe di bit con elevata lunghezza e linguaggi di dominio specifico. In questo progetto introduciamo il "deep modelling", un approccio che integra la modellazione simbolica con le procedure decisionali utilizzate per controllare i modelli dei sistemi. Il nostro obiettivo è quello di andare oltre gli approcci tradizionali della verifica di sistemi hardware, introducendo un sistema rigoroso che è stato pensato sin dall'inizio per supportare la verifica del software. Il nostro approccio richiede una profonda comprensione sia di come modellare il programma, che delle procedure decisionali, sviluppandosi in due passi: la raccolta di informazioni dal dominio specifico per ottenere astrazioni più efficienti, e lo studio di modifiche alle procedure decisionali in modo che possano adattarsi meglio al modello da risolvere. Riteniamo che questa ricerca avrà un forte impatto su questo campo, attualmente in rapido sviluppo e che ha un ruolo sempre più importante nella società in generale.
Direct link to Lay Summary Last update: 09.09.2019

Responsible applicant and co-applicants

Employees

Project partner

Associated projects

Number Title Start Funding scheme
166288 From Parallel SMT to Parallel Software Verification 01.09.2017 Project funding (Div. I-III)

Abstract

Formal verification of software, developed from a highly successful field of hardware verification, is currently facing an explosion in the number of safety critical applications written in programming languages that are increasingly far from hardware. For instance, the emergence of large-scale distributed consensus algorithms and their applications to smart contracts have not only created wholly new research questions but also challenged the way in which verification is currently being done, due to their use of high bit-widths and application-specic languages. In this proposal we outline deep modelling, a new approach that integrates symbolic modelling and the decision procedures used for solving the models. Our goal is to go beyond the traditional approaches originating from hardware model checking by introducing a rigorous system that is built from the beginning to support software verification. The outlined approach requires a deep understanding of both model checking and decision procedures due to it being fundamentally two-fold:we take information from the domain to obtain more efficient abstractions; and we study changes to the decision procedures so that they can better adjust to the model beingsolved.
-